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 p being non constant Element of the carrier of (Polynom-Ring F) st p splits_in E holds
h .: (Roots (E,p)) 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 p being non constant Element of the carrier of (Polynom-Ring F) st p splits_in E holds
h .: (Roots (E,p)) c= the carrier of E
let K be F -extending FieldExtension of F; :: thesis: for h being F -fixing Monomorphism of E,K
for p being non constant Element of the carrier of (Polynom-Ring F) st p splits_in E holds
h .: (Roots (E,p)) c= the carrier of E
let h be F -fixing Monomorphism of E,K; :: thesis: for p being non constant Element of the carrier of (Polynom-Ring F) st p splits_in E holds
h .: (Roots (E,p)) c= the carrier of E
let p be non constant Element of the carrier of (Polynom-Ring F); :: thesis: ( p splits_in E implies h .: (Roots (E,p)) c= the carrier of E )
assume AS: p splits_in E ; :: thesis: h .: (Roots (E,p)) c= the carrier of E
H: ( Roots (E,p) = { a where a is Element of E : a is_a_root_of p,E } & Roots (K,p) = { a where a is Element of K : a is_a_root_of p,K } ) by FIELD_4:def 4;

now :: thesis: for o being object st o in h .: (Roots (E,p)) holds
o in the carrier of E

let o be object ; :: thesis: ( o in h .: (Roots (E,p)) implies o in the carrier of E )
assume o in h .: (Roots (E,p)) ; :: thesis: o in the carrier of E
then consider x being object such that
B: ( x in dom h & x in Roots (E,p) & o = h . x ) by FUNCT_1:def 6;
consider a being Element of E such that
C: ( a = x & a is_a_root_of p,E ) by B, H;
Ext_eval (p,a) = 0. E by C, FIELD_4:def 2;
then 0. K = h . (Ext_eval (p,a)) by RING_2:6
.= Ext_eval (p,(h . a)) by fixeval ;
then h . a is_a_root_of p,K by FIELD_4:def 2;
then h . a in Roots (K,p) by H;
then h . a in Roots (E,p) by AS, lemNor2bb;
hence o in the carrier of E by C, B; :: thesis: verum

end;

hence h .: (Roots (E,p)) c= the carrier of E ; :: thesis: verum