let F be Field; :: thesis: for E being FieldExtension of F
for a being Element of E holds
( a is F -algebraic iff ex B being F -finite FieldExtension of F st
( E is B -extending & a in B ) )
let E be FieldExtension of F; :: thesis: for a being Element of E holds
( a is F -algebraic iff ex B being F -finite FieldExtension of F st
( E is B -extending & a in B ) )
let a be Element of E; :: thesis: ( a is F -algebraic iff ex B being F -finite FieldExtension of F st
( E is B -extending & a in B ) )

A: now :: thesis: ( a is F -algebraic implies ex B being F -finite FieldExtension of F st
( E is B -extending & a in B ) )

assume A0: a is F -algebraic ; :: thesis: ex B being F -finite FieldExtension of F st
( E is B -extending & a in B )
A1: {a} is Subset of (FAdj (F,{a})) by FIELD_6:35;
FAdj (F,{a}) is Subring of E by FIELD_5:12;
then A2: E is FAdj (F,{a}) -extending by FIELD_4:def 1;
a in {a} by TARSKI:def 1;
then a in FAdj (F,{a}) by A1;
hence ex B being F -finite FieldExtension of F st
( E is B -extending & a in B ) by A0, A2; :: thesis: verum

end;

now :: thesis: ( ex B being F -finite FieldExtension of F st
( E is B -extending & a in B ) implies a is F -algebraic )

assume ex B being F -finite FieldExtension of F st
( E is B -extending & a in B ) ; :: thesis: a is F -algebraic
then consider B being F -finite FieldExtension of F such that
A0: ( E is B -extending & a in B ) ;
reconsider E1 = E as B -extending FieldExtension of F by A0;
reconsider a1 = a as B -membered Element of E1 by A0, defmem;
@ ((@ (B,a1)),E1) is F -algebraic ;
hence a is F -algebraic ; :: thesis: verum

end;

hence ( a is F -algebraic iff ex B being F -finite FieldExtension of F st
( E is B -extending & a in B ) ) by A; :: thesis: verum