let F be Field; :: thesis: for E being F -algebraic FieldExtension of F
for h being F -fixing Monomorphism of E holds the carrier of E c= rng h
let E be F -algebraic FieldExtension of F; :: thesis: for h being F -fixing Monomorphism of E holds the carrier of E c= rng h
let h be F -fixing Monomorphism of E; :: thesis: the carrier of E c= rng h

now :: thesis: for o being object st o in the carrier of E holds
o in rng h

let o be object ; :: thesis: ( o in the carrier of E implies o in rng h )
assume o in the carrier of E ; :: thesis: o in rng h
then reconsider a = o as Element of E ;
set p = MinPoly (a,F);
set M = Roots (E,(MinPoly (a,F)));
H: Roots (E,(MinPoly (a,F))) = { a where a is Element of E : a is_a_root_of MinPoly (a,F),E } by FIELD_4:def 4;
Ext_eval ((MinPoly (a,F)),a) = 0. E by FIELD_6:52;
then a is_a_root_of MinPoly (a,F),E by FIELD_4:def 2;
then a in Roots (E,(MinPoly (a,F))) by H;
then a in h .: (Roots (E,(MinPoly (a,F)))) by fixrr;
then consider x being object such that
A: ( x in dom h & x in Roots (E,(MinPoly (a,F))) & a = h . x ) by FUNCT_1:def 6;
thus o in rng h by A, FUNCT_1:def 3; :: thesis: verum

end;

hence the carrier of E c= rng h ; :: thesis: verum