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

now :: thesis: ( ( for a being Element of E holds FAdj (F,{a}) is F -finite ) implies E is F -algebraic )

assume A: for a being Element of E holds FAdj (F,{a}) is F -finite ; :: thesis: E is F -algebraic

now :: thesis: for a being Element of E holds a is F -algebraic

let a be Element of E; :: thesis: a is F -algebraic
FAdj (F,{a}) is F -finite by A;
hence a is F -algebraic by FIELD_6:68; :: thesis: verum

end;

hence E is F -algebraic ; :: thesis: verum

end;

hence ( E is F -algebraic iff for a being Element of E holds FAdj (F,{a}) is F -finite ) ; :: thesis: verum