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
let x be set ; :: according to FUNCT_1:def 8 :: thesis: for b₁ being set holds
( not x in dom (Sgm A) or not b₁ in dom (Sgm A) or not (Sgm A) . x = (Sgm A) . b₁ or x = b₁ )
let y be set ; :: 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
A2: ( x in dom (Sgm A) & y in dom (Sgm A) ) and
A3: (Sgm A) . x = (Sgm A) . y and
A4: x <> y ; :: thesis: contradiction
A5: dom (Sgm A) = Seg (len (Sgm A)) by FINSEQ_1:def 3;
reconsider i = x, j = y as Element of NAT by A2;
( (Sgm A) . x in rng (Sgm A) & (Sgm A) . y in rng (Sgm A) & rng (Sgm A) = A ) by A1, A2, FINSEQ_1:def 13, FUNCT_1:def 5;
then ( (Sgm A) . x in Seg k & (Sgm A) . y in Seg k ) by A1;
then reconsider m = (Sgm A) . x, n = (Sgm A) . y as Element of NAT ;

now

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

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

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

end;

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

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

end;

end;

end;

hence contradiction ; :: thesis: verum