thus
( IT is one-to-one implies for n, m being Element of NAT st 1 <= n & n < m & m <= len IT holds
IT . n <> IT . m )
:: thesis: ( ( for n, m being Element of NAT st 1 <= n & n < m & m <= len IT holds
IT . n <> IT . m ) implies IT is one-to-one )proof
assume A1:
IT is
one-to-one
;
:: thesis: for n, m being Element of NAT st 1 <= n & n < m & m <= len IT holds
IT . n <> IT . m
let n,
m be
Element of
NAT ;
:: thesis: ( 1 <= n & n < m & m <= len IT implies IT . n <> IT . m )
assume that A2:
1
<= n
and A3:
n < m
and A4:
m <= len IT
;
:: thesis: IT . n <> IT . m
A5:
n <= len IT
by A3, A4, XXREAL_0:2;
A6:
1
<= m
by A2, A3, XXREAL_0:2;
A7:
n in dom IT
by A2, A5, FINSEQ_3:27;
A8:
m in dom IT
by A4, A6, FINSEQ_3:27;
thus
IT . n <> IT . m
by A1, A3, A7, A8, FUNCT_1:def 8;
:: thesis: verum
end;
assume A9:
for n, m being Element of NAT st 1 <= n & n < m & m <= len IT holds
IT . n <> IT . m
; :: thesis: IT is one-to-one
let x1, x2 be set ; :: according to FUNCT_1:def 8 :: thesis: ( not x1 in dom IT or not x2 in dom IT or not IT . x1 = IT . x2 or x1 = x2 )
assume that
A10:
( x1 in dom IT & x2 in dom IT )
and
A11:
IT . x1 = IT . x2
; :: thesis: x1 = x2
reconsider x' = x1, y' = x2 as Element of NAT by A10;
A12:
( x' <= len IT & 1 <= y' )
by A10, FINSEQ_3:27;
A13:
( 1 <= x' & y' <= len IT )
by A10, FINSEQ_3:27;