let F be Field; :: thesis: for E being FieldExtension of F
for a being F -algebraic Element of E holds
( E == FAdj (F,{a}) iff deg (MinPoly (a,F)) = deg (E,F) )
let E be FieldExtension of F; :: thesis: for a being F -algebraic Element of E holds
( E == FAdj (F,{a}) iff deg (MinPoly (a,F)) = deg (E,F) )
let a be F -algebraic Element of E; :: thesis: ( E == FAdj (F,{a}) iff deg (MinPoly (a,F)) = deg (E,F) )

A: now :: thesis: ( E == FAdj (F,{a}) implies deg (MinPoly (a,F)) = deg (E,F) )

assume A0: E == FAdj (F,{a}) ; :: thesis: deg (MinPoly (a,F)) = deg (E,F)
deg ((FAdj (F,{a})),F) = deg (MinPoly (a,F)) by FIELD_6:67;
hence deg (MinPoly (a,F)) = deg (E,F) by A0, str11; :: thesis: verum

end;

now :: thesis: ( deg (MinPoly (a,F)) = deg (E,F) implies E == FAdj (F,{a}) )

assume B0: deg (MinPoly (a,F)) = deg (E,F) ; :: thesis: E == FAdj (F,{a})
reconsider Fa = FAdj (F,{a}) as FieldExtension of F ;
reconsider E1 = E as Fa -extending FieldExtension of F by FIELD_4:7;
VecSp (E1,F) is finite-dimensional by B0, FIELD_4:def 7;
then E1 is F -finite by FIELD_4:def 8;
then reconsider E1 = E as F -extending FAdj (F,{a}) -finite FieldExtension of F by alg0;
reconsider d1 = deg (E,F) as non zero Nat by B0;
deg (E,F) = (deg (E1,(FAdj (F,{a})))) * (deg ((FAdj (F,{a})),F)) by degmult
.= (deg (E1,(FAdj (F,{a})))) * (deg (E,F)) by B0, FIELD_6:67 ;
hence E == FAdj (F,{a}) by str1a, XCMPLX_1:7; :: thesis: verum

end;

hence ( E == FAdj (F,{a}) iff deg (MinPoly (a,F)) = deg (E,F) ) by A; :: thesis: verum