let F be Field; :: thesis: for E being F -finite FieldExtension of F holds
( E is F -simple iff ex a being Element of E st deg (a,F) = deg (E,F) )
let E be F -finite FieldExtension of F; :: thesis: ( E is F -simple iff ex a being Element of E st deg (a,F) = deg (E,F) )

A: now :: thesis: ( E is F -simple implies ex a being Element of E st deg (a,F) = deg (E,F) )

assume E is F -simple ; :: thesis: ex a being Element of E st deg (a,F) = deg (E,F)
then consider a being Element of E such that
A1: E == FAdj (F,{a}) ;
deg (E,F) = deg (a,F) by A1, FIELD_7:5;
hence ex a being Element of E st deg (a,F) = deg (E,F) ; :: thesis: verum

end;

now :: thesis: ( ex a being Element of E st deg (a,F) = deg (E,F) implies E is F -simple )

assume ex a being Element of E st deg (a,F) = deg (E,F) ; :: thesis: E is F -simple
then consider a being Element of E such that
A2: deg (a,F) = deg (E,F) ;
set K = FAdj (F,{a});
reconsider E1 = E as F -extending FAdj (F,{a}) -finite FieldExtension of F by FIELD_4:7, FIELD_7:31;
(deg ((FAdj (F,{a})),F)) * ((deg ((FAdj (F,{a})),F)) ") = ((deg (E1,(FAdj (F,{a})))) * (deg ((FAdj (F,{a})),F))) * ((deg ((FAdj (F,{a})),F)) ") by A2, FIELD_7:30
.= (deg (E1,(FAdj (F,{a})))) * ((deg ((FAdj (F,{a})),F)) / (deg ((FAdj (F,{a})),F)))
.= (deg (E1,(FAdj (F,{a})))) * 1 by XCMPLX_1:60 ;
then deg (E1,(FAdj (F,{a}))) = (deg ((FAdj (F,{a})),F)) / (deg ((FAdj (F,{a})),F))
.= 1 by XCMPLX_1:60 ;
hence E is F -simple by FIELD_7:8; :: thesis: verum

end;

hence ( E is F -simple iff ex a being Element of E st deg (a,F) = deg (E,F) ) by A; :: thesis: verum