Definition. degree of field extensions [1203]