consider k being Nat such that
A1: A c= k by AE221f;
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

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
A2: ( x in dom (Sgm0 A) & y in dom (Sgm0 A) ) and
A3: (Sgm0 A) . x = (Sgm0 A) . y and
A4: x <> y ; :: thesis: contradiction
reconsider i = x, j = y as Element of NAT by A2;
reconsider k0 = k as Element of NAT by ORDINAL1:def 13;
( (Sgm0 A) . x in rng (Sgm0 A) & (Sgm0 A) . y in rng (Sgm0 A) & rng (Sgm0 A) = A ) by A2, AC113, FUNCT_1:def 5;
then reconsider m = (Sgm0 A) . x, n = (Sgm0 A) . y as Element of NAT by A1, AB470;

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

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

j < len (Sgm0 A) by A2, NAT_1:45;
hence contradiction by A6, AC113, A3; :: thesis: verum

end;

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

i < len (Sgm0 A) by A2, NAT_1:45;
hence contradiction by A7, AC113, A3; :: thesis: verum

end;

end;

end;

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