let K be Field; :: thesis: for F being K -monomorphic Field
for f being Monomorphism of K,F st K,F are_disjoint holds
emb_iso f is onto
let F be K -monomorphic Field; :: thesis: for f being Monomorphism of K,F st K,F are_disjoint holds
emb_iso f is onto
let f be Monomorphism of K,F; :: thesis: ( K,F are_disjoint implies emb_iso f is onto )
assume AS: K,F are_disjoint ; :: thesis: emb_iso f is onto
set g = emb_iso f;
E: [#] (embField f) = carr f by defemb;
F: dom (emb_iso f) = [#] (embField f) by FUNCT_2:def 1;

A: now :: thesis: for o being object st o in [#] F holds
o in rng (emb_iso f)

let o be object ; :: thesis: ( o in [#] F implies b₁ in rng (emb_iso f) )
assume o in [#] F ; :: thesis: b₁ in rng (emb_iso f)
then reconsider u = o as Element of F ;

per cases ( u in rng f or not u in rng f ) ;

suppose u in rng f ; :: thesis: b₁ in rng (emb_iso f)

then consider y being object such that
B: ( y in dom f & f . y = u ) by FUNCT_1:def 3;
reconsider y = y as Element of K by B;
reconsider yy = y as Element of (embField f) by E, XBOOLE_0:def 3;
y in K ;
then (emb_iso f) . yy = u by B, defiso;
hence o in rng (emb_iso f) by F, FUNCT_1:3; :: thesis: verum

end;

suppose not u in rng f ; :: thesis: b₁ in rng (emb_iso f)

then u in ([#] F) \ (rng f) by XBOOLE_0:def 5;
then reconsider uu = u as Element of (embField f) by E, XBOOLE_0:def 3;
not u in K by AS, XBOOLE_0:def 4;
then (emb_iso f) . uu = u by defiso;
hence o in rng (emb_iso f) by F, FUNCT_1:3; :: thesis: verum

end;

end;

end;

for o being object st o in rng (emb_iso f) holds
o in [#] F ;
hence emb_iso f is onto by A, TARSKI:2; :: thesis: verum