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

now :: thesis: ( deg (a,F) = deg (E,F) implies a is F -primitive )

assume AS: deg (a,F) = deg (E,F) ; :: thesis: a is F -primitive
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 AS, 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 a is F -primitive by FIELD_7:8; :: thesis: verum

end;

hence ( a is F -primitive iff deg (a,F) = deg (E,F) ) by FIELD_7:5; :: thesis: verum