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 non empty finite F -algebraic Subset of E holds h .: the carrier of (FAdj (F,T)) c= the carrier of (FAdj (F,(h .: T)))
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 non empty finite F -algebraic Subset of E holds h .: the carrier of (FAdj (F,T)) c= the carrier of (FAdj (F,(h .: T)))
let K be F -extending FieldExtension of F; :: thesis: for h being F -fixing Monomorphism of E,K
for T being non empty finite F -algebraic Subset of E holds h .: the carrier of (FAdj (F,T)) c= the carrier of (FAdj (F,(h .: T)))
let h be F -fixing Monomorphism of E,K; :: thesis: for T being non empty finite F -algebraic Subset of E holds h .: the carrier of (FAdj (F,T)) c= the carrier of (FAdj (F,(h .: T)))
let T be non empty finite F -algebraic Subset of E; :: thesis: h .: the carrier of (FAdj (F,T)) c= the carrier of (FAdj (F,(h .: T)))
h .: T is F -algebraic by ll;
then A0: FAdj (F,(h .: T)) = RAdj (F,(h .: T)) by help1;

now :: thesis: for o being object st o in h .: the carrier of (FAdj (F,T)) holds
o in the carrier of (FAdj (F,(h .: T)))

let o be object ; :: thesis: ( o in h .: the carrier of (FAdj (F,T)) implies o in the carrier of (FAdj (F,(h .: T))) )
assume o in h .: the carrier of (FAdj (F,T)) ; :: thesis: o in the carrier of (FAdj (F,(h .: T)))
then consider a being object such that
A1: ( a in dom h & a in the carrier of (FAdj (F,T)) & o = h . a ) by FUNCT_1:def 6;
reconsider a = a as Element of (FAdj (F,T)) by A1;
FAdj (F,T) = RAdj (F,T) by help1;
then consider p being Polynomial of (card T),F, x being T -evaluating Function of (card T),E such that
A2: a = Ext_eval (p,x) by help2;
thus o in the carrier of (FAdj (F,(h .: T))) by A0, A1, A2, help3; :: thesis: verum

end;

hence h .: the carrier of (FAdj (F,T)) c= the carrier of (FAdj (F,(h .: T))) ; :: thesis: verum