consider k being Nat such that
A1: A c= Seg k by FINSEQ_1:def 13;
A2: rng (Sgm A) = A by FINSEQ_1:def 14;
let x, y be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x in dom (Sgm A) or not y in dom (Sgm A) or not (Sgm A) . x = (Sgm A) . y or x = y )
assume that
A3: x in dom (Sgm A) and
A4: y in dom (Sgm A) and
A5: (Sgm A) . x = (Sgm A) . y and
A6: x <> y ; :: thesis: contradiction
(Sgm A) . y in rng (Sgm A) by A4, FUNCT_1:def 3;
then A7: (Sgm A) . y in Seg k by A1, A2;
(Sgm A) . x in rng (Sgm A) by A3, FUNCT_1:def 3;
then (Sgm A) . x in Seg k by A1, A2;
then reconsider m = (Sgm A) . x, n = (Sgm A) . y as Element of NAT by A7;
reconsider i = x, j = y as Element of NAT by A3, A4;
A8: dom (Sgm A) = Seg (len (Sgm A)) by FINSEQ_1:def 3;

now :: thesis: contradiction

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

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

A10: j <= len (Sgm A) by A4, A8, FINSEQ_1:1;
1 <= i by A3, A8, FINSEQ_1:1;
then m < n by A9, A10, FINSEQ_1:def 14;
hence contradiction by A5; :: thesis: verum

end;

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

A12: i <= len (Sgm A) by A3, A8, FINSEQ_1:1;
1 <= j by A4, A8, FINSEQ_1:1;
then n < m by A11, A12, FINSEQ_1:def 14;
hence contradiction by A5; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum