for x, y being object 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 object ; :: thesis: ( x in dom (Sgm0 A) & y in dom (Sgm0 A) & (Sgm0 A) . x = (Sgm0 A) . y implies not x <> y )
assume that
A1: x in dom (Sgm0 A) and
A2: 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 A1, A2;

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

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

j < len (Sgm0 A) by A2, AFINSQ_1:86;
hence contradiction by A3, A5, Def4; :: thesis: verum

end;

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

i < len (Sgm0 A) by A1, AFINSQ_1:86;
hence contradiction by A3, A6, Def4; :: thesis: verum

end;

end;

end;

hence Sgm0 A is one-to-one ; :: thesis: verum