thus ( IT is one-to-one implies for n, m being Nat st 1 <= n & n < m & m <= len IT holds
IT . n <> IT . m ) :: thesis: ( ( for n, m being 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 Nat st 1 <= n & n < m & m <= len IT holds
IT . n <> IT . m
let n, m be 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:25;
m in dom IT by A4, A6, FINSEQ_3:25;
hence IT . n <> IT . m by A1, A3, A7; :: thesis: verum

end;

assume A8: for n, m being Nat st 1 <= n & n < m & m <= len IT holds
IT . n <> IT . m ; :: thesis: IT is one-to-one
let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x1 in dom IT or not x2 in dom IT or not IT . x1 = IT . x2 or x1 = x2 )
assume that
A9: ( x1 in dom IT & x2 in dom IT ) and
A10: IT . x1 = IT . x2 ; :: thesis: x1 = x2
reconsider x9 = x1, y9 = x2 as Element of NAT by A9;
A11: ( x9 <= len IT & 1 <= y9 ) by A9, FINSEQ_3:25;
A12: ( 1 <= x9 & y9 <= len IT ) by A9, FINSEQ_3:25;

per cases ( x9 <> y9 or x9 = y9 ) ;

suppose A13: x9 <> y9 ; :: thesis: x1 = x2

now :: thesis: x1 = x2

per cases ( x9 < y9 or y9 < x9 ) by A13, XXREAL_0:1;

suppose x9 < y9 ; :: thesis: x1 = x2

hence x1 = x2 by A8, A10, A12; :: thesis: verum

end;

suppose y9 < x9 ; :: thesis: x1 = x2

hence x1 = x2 by A8, A10, A11; :: thesis: verum

end;

end;

end;

hence x1 = x2 ; :: thesis: verum

end;

suppose x9 = y9 ; :: thesis: x1 = x2

hence x1 = x2 ; :: thesis: verum

end;

end;