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 A2: ( 1 <= n & n < m & m <= len IT ) ; :: thesis: IT . n <> IT . m
then ( n <= len IT & 1 <= m ) by XXREAL_0:2;
then ( n in dom IT & m in dom IT & n <> m ) by A2, FINSEQ_3:27;
hence IT . n <> IT . m by A1, FUNCT_1:def 8; :: thesis: verum

end;

assume A3: 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 A4: ( x1 in dom IT & x2 in dom IT & IT . x1 = IT . x2 ) ; :: thesis: x1 = x2
then reconsider x' = x1, y' = x2 as Element of NAT ;
A5: ( 1 <= x' & x' <= len IT & 1 <= y' & y' <= len IT ) by A4, FINSEQ_3:27;

per cases ( x' <> y' or x' = y' ) ;

suppose A6: x' <> y' ; :: thesis: x1 = x2

now

per cases ( x' < y' or y' < x' ) by A6, XXREAL_0:1;

suppose x' < y' ; :: thesis: x1 = x2

hence x1 = x2 by A3, A4, A5; :: thesis: verum

end;

suppose y' < x' ; :: thesis: x1 = x2

hence x1 = x2 by A3, A4, A5; :: thesis: verum

end;

end;

end;

hence x1 = x2 ; :: thesis: verum

end;

suppose x' = y' ; :: thesis: x1 = x2

hence x1 = x2 ; :: thesis: verum

end;

end;