let K be Field; :: thesis:
let F be K -monomorphic Field; :: thesis:
let f be Monomorphism of K,F; :: thesis:
assume AS: K,F are_disjoint ; :: thesis:
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:

let o be object ; :: thesis:
assume o in [#] F ; :: thesis:
then reconsider u = o as Element of F ;

suppose u in rng f ; :: thesis:

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:

end;

suppose not u in rng f ; :: thesis:

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:

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: