let A be set ; :: thesis: for k being natural number st A c= Seg k holds
Sgm A is one-to-one
let k be natural number ; :: thesis: ( A c= Seg k implies Sgm A is one-to-one )
assume A1: A c= Seg k ; :: thesis: Sgm A is one-to-one
then A2: rng (Sgm A) = A by FINSEQ_1:def 13;
let x be set ; :: according to FUNCT_1:def 8 :: thesis: for b₁ being set holds
( not x in proj1 (Sgm A) or not b₁ in proj1 (Sgm A) or not (Sgm A) . x = (Sgm A) . b₁ or x = b₁ )
let y be set ; :: thesis: ( not x in proj1 (Sgm A) or not y in proj1 (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 5;
then A7: (Sgm A) . y in Seg k by A1, A2;
(Sgm A) . x in rng (Sgm A) by A3, FUNCT_1:def 5;
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

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:3;
1 <= i by A3, A8, FINSEQ_1:3;
then m < n by A1, A9, A10, FINSEQ_1:def 13;
hence contradiction by A5; :: thesis: verum

end;

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

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

end;

end;

end;

hence contradiction ; :: thesis: verum