let F be Field; :: thesis: for E being FieldExtension of F
for K being F -extending FieldExtension of F
for h being F -fixing Monomorphism of E,K
for T being F -algebraic Subset of E holds h .: T is F -algebraic
let E be FieldExtension of F; :: thesis: for K being F -extending FieldExtension of F
for h being F -fixing Monomorphism of E,K
for T being F -algebraic Subset of E holds h .: T is F -algebraic
let K be F -extending FieldExtension of F; :: thesis: for h being F -fixing Monomorphism of E,K
for T being F -algebraic Subset of E holds h .: T is F -algebraic
let h be F -fixing Monomorphism of E,K; :: thesis: for T being F -algebraic Subset of E holds h .: T is F -algebraic
let T be F -algebraic Subset of E; :: thesis: h .: T is F -algebraic

now :: thesis: for a being Element of K st a in h .: T holds
a is F -algebraic

let a be Element of K; :: thesis: ( a in h .: T implies a is F -algebraic )
assume a in h .: T ; :: 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 Element of E by A;
consider p being non zero Polynomial of F such that
B: Ext_eval (p,x) = 0. E by A, FIELD_6:43;
p is Element of the carrier of (Polynom-Ring F) by POLYNOM3:def 10;
then Ext_eval (p,a) = h . (0. E) by A, B, fixeval
.= 0. K by RING_2:6 ;
hence a is F -algebraic by FIELD_6:43; :: thesis: verum

end;

hence h .: T is F -algebraic by FIELD_7:def 12; :: thesis: verum