set g = emb_iso f;
E: [#] (embField f) = carr f by defemb;
D: dom f = [#] K by FUNCT_2:def 1;
H: f is one-to-one ;

now :: thesis: for x1, x2 being object st x1 in dom (emb_iso f) & x2 in dom (emb_iso f) & (emb_iso f) . x1 = (emb_iso f) . x2 holds
x1 = x2

let x1, x2 be object ; :: thesis: ( x1 in dom (emb_iso f) & x2 in dom (emb_iso f) & (emb_iso f) . x1 = (emb_iso f) . x2 implies b₁ = b₂ )
assume A: ( x1 in dom (emb_iso f) & x2 in dom (emb_iso f) & (emb_iso f) . x1 = (emb_iso f) . x2 ) ; :: thesis: b₁ = b₂
then reconsider c = x2 as Element of (embField f) ;

per cases ( x1 in [#] K or not x1 in [#] K ) ;

suppose x1 in [#] K ; :: thesis: b₁ = b₂

then reconsider a = x1 as Element of K ;
a in K ;
then B: f . a = (emb_iso f) . a by A, defiso;
then C: (emb_iso f) . a in rng f by D, FUNCT_1:def 3;

now :: thesis: x2 in K

assume C1: not x2 in K ; :: thesis: contradiction
(emb_iso f) . c = x2 by C1, defiso;
then not x2 in ([#] F) \ (rng f) by C, A, XBOOLE_0:def 5;
hence contradiction by C1, A, E, XBOOLE_0:def 3; :: thesis: verum

end;

then reconsider b = x2 as Element of K ;
b in K ;
then f . b = f . a by A, B, defiso;
hence x1 = x2 by H, D; :: thesis: verum

end;

suppose Z: not x1 in [#] K ; :: thesis: b₁ = b₂

reconsider a = x1 as Element of (embField f) by A;
not a in K by Z;
then B: (emb_iso f) . a = a by defiso;

now :: thesis: not x2 in K

assume C1: x2 in K ; :: thesis: contradiction
then C2: x2 in dom f by FUNCT_2:def 1;
reconsider c = x2 as Element of (embField f) by A;
a = f . x2 by A, B, C1, defiso;
then a in rng f by C2, FUNCT_1:def 3;
then not a in ([#] F) \ (rng f) by XBOOLE_0:def 5;
hence contradiction by Z, E, XBOOLE_0:def 3; :: thesis: verum

end;

hence x1 = x2 by A, B, defiso; :: thesis: verum

end;

end;

end;

hence emb_iso f is one-to-one ; :: thesis: verum