let A be set ; for k being Nat st A c= Seg k holds
Sgm A is one-to-one
let k be Nat; ( A c= Seg k implies Sgm A is one-to-one )
assume A1:
A c= Seg k
; Sgm A is one-to-one
then A2:
rng (Sgm A) = A
by FINSEQ_1:def 13;
let x, y be object ; FUNCT_1:def 4 ( 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
; 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;
hence
contradiction
; verum