let F be Field; :: thesis: for E being FieldExtension of F
for K being b₁ -extending FieldExtension of F
for T being finite F -algebraic Subset of K st T c= the carrier of E holds
FAdj (F,T) is Subfield of E
let E be FieldExtension of F; :: thesis: for K being E -extending FieldExtension of F
for T being finite F -algebraic Subset of K st T c= the carrier of E holds
FAdj (F,T) is Subfield of E
let K be E -extending FieldExtension of F; :: thesis: for T being finite F -algebraic Subset of K st T c= the carrier of E holds
FAdj (F,T) is Subfield of E
let T be finite F -algebraic Subset of K; :: thesis: ( T c= the carrier of E implies FAdj (F,T) is Subfield of E )
assume T c= the carrier of E ; :: thesis: FAdj (F,T) is Subfield of E
then reconsider T1 = T as finite Subset of E ;

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

let a be Element of E; :: thesis: ( a in T1 implies a is F -algebraic )
assume A: a in T1 ; :: thesis: a is F -algebraic
then reconsider b = a as Element of K ;
consider p being non zero Polynomial of F such that
B: Ext_eval (p,b) = 0. K by A, FIELD_6:43;
reconsider p = p as non zero Element of the carrier of (Polynom-Ring F) by POLYNOM3:def 10;
C: E is Subfield of K by FIELD_4:7;
Ext_eval (p,a) = Ext_eval (p,b) by FIELD_6:11
.= 0. E by B, C, EC_PF_1:def 1 ;
hence a is F -algebraic by FIELD_6:43; :: thesis: verum

end;

then reconsider T1 = T1 as finite F -algebraic Subset of E by FIELD_7:def 12;
FAdj (F,T1) = FAdj (F,T) by lemh1;
hence FAdj (F,T) is Subfield of E ; :: thesis: verum