consider k being Nat such that
A1: A c= k by Th2;
for x, y being set st x in dom (Sgm0 A) & y in dom (Sgm0 A) & (Sgm0 A) . x = (Sgm0 A) . y holds
not x <> y

proof

A2: rng (Sgm0 A) = A by Def5;
reconsider k0 = k as Element of NAT by ORDINAL1:def 13;
let x, y be set ; :: thesis: ( x in dom (Sgm0 A) & y in dom (Sgm0 A) & (Sgm0 A) . x = (Sgm0 A) . y implies not x <> y )
assume that
A3: x in dom (Sgm0 A) and
A4: y in dom (Sgm0 A) and
A5: (Sgm0 A) . x = (Sgm0 A) . y and
A6: x <> y ; :: thesis: contradiction
A7: (Sgm0 A) . y in rng (Sgm0 A) by A4, FUNCT_1:def 5;
(Sgm0 A) . x in rng (Sgm0 A) by A3, FUNCT_1:def 5;
then reconsider m = (Sgm0 A) . x, n = (Sgm0 A) . y as Element of NAT by A1, A7, A2, Th1;
reconsider i = x, j = y as Element of NAT by A3, A4;

per cases ( i < j or j < i ) by A6, XXREAL_0:1;

suppose A8: i < j ; :: thesis: contradiction

j < len (Sgm0 A) by A4, NAT_1:45;
hence contradiction by A5, A8, Def5; :: thesis: verum

end;

suppose A9: j < i ; :: thesis: contradiction

i < len (Sgm0 A) by A3, NAT_1:45;
hence contradiction by A5, A9, Def5; :: thesis: verum

end;

end;

end;

hence Sgm0 A is one-to-one by FUNCT_1:def 8; :: thesis: verum