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

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 in T1 ; :: thesis: a is F -algebraic
then consider x being object such that
A: ( x in dom h & x in T & a = h . x ) by FUNCT_1:def 6;
reconsider x = x as F -algebraic Element of E by A;
consider p being non zero Polynomial of F such that
B: Ext_eval (p,x) = 0. E by 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,(h . x)) by A, FIELD_6:11
.= h . (0. E) by B, fixeval
.= 0. K by RING_2:6
.= 0. E by 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,(h .: T)) by lemh1;
hence FAdj (F,(h .: T)) is Subfield of E ; :: thesis: verum