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 st h .: T c= the carrier of E holds
h .: the carrier of (FAdj (F,T)) c= the carrier of E
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 st h .: T c= the carrier of E holds
h .: the carrier of (FAdj (F,T)) c= the carrier of E
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 st h .: T c= the carrier of E holds
h .: the carrier of (FAdj (F,T)) c= the carrier of E
let h be F -fixing Monomorphism of E,K; :: thesis: for T being non empty finite F -algebraic Subset of E st h .: T c= the carrier of E holds
h .: the carrier of (FAdj (F,T)) c= the carrier of E
let T be non empty finite F -algebraic Subset of E; :: thesis: ( h .: T c= the carrier of E implies h .: the carrier of (FAdj (F,T)) c= the carrier of E )
assume h .: T c= the carrier of E ; :: thesis: h .: the carrier of (FAdj (F,T)) c= the carrier of E
then FAdj (F,(h .: T)) is Subfield of E by lemh;
then A: the carrier of (FAdj (F,(h .: T))) c= the carrier of E by EC_PF_1:def 1;
h .: the carrier of (FAdj (F,T)) c= the carrier of (FAdj (F,(h .: T))) by lemNor2ch;
hence h .: the carrier of (FAdj (F,T)) c= the carrier of E by A; :: thesis: verum