let p be FinSequence; :: thesis: ( ( for n, m being Element of NAT st 1 <= n & n < m & m <= len p holds
p . n <> p . m ) iff p is one-to-one )

hereby :: thesis: ( p is one-to-one implies for n, m being Element of NAT st 1 <= n & n < m & m <= len p holds
p . n <> p . m )

assume A1: for n, m being Element of NAT st 1 <= n & n < m & m <= len p holds
p . n <> p . m ; :: thesis: p is one-to-one
thus p is one-to-one :: thesis: verum

proof

let x1, x2 be set ; :: according to FUNCT_1:def 8 :: thesis: ( not x1 in dom p or not x2 in dom p or not p . x1 = p . x2 or x1 = x2 )
assume A2: ( x1 in dom p & x2 in dom p & p . x1 = p . x2 ) ; :: thesis: x1 = x2
assume A3: x1 <> x2 ; :: thesis: contradiction
reconsider n = x1, m = x2 as Element of NAT by A2;
A4: ( 1 <= n & n <= len p ) by A2, FINSEQ_3:27;
A5: ( 1 <= m & m <= len p ) by A2, FINSEQ_3:27;

per cases ( m <= n or m > n ) ;

suppose m <= n ; :: thesis: contradiction

then m < n by A3, XXREAL_0:1;
hence contradiction by A1, A2, A4, A5; :: thesis: verum

end;

suppose m > n ; :: thesis: contradiction

hence contradiction by A1, A2, A4, A5; :: thesis: verum

end;

end;

end;

end;

assume A6: p is one-to-one ; :: thesis: for n, m being Element of NAT st 1 <= n & n < m & m <= len p holds
p . n <> p . m
let n, m be Element of NAT ; :: thesis: ( 1 <= n & n < m & m <= len p implies p . n <> p . m )
assume A7: ( 1 <= n & n < m & m <= len p ) ; :: thesis: p . n <> p . m
assume A8: p . n = p . m ; :: thesis: contradiction
n <= len p by A7, XXREAL_0:2;
then A9: n in dom p by A7, FINSEQ_3:27;
1 <= m by A7, XXREAL_0:2;
then m in dom p by A7, FINSEQ_3:27;
hence contradiction by A6, A7, A8, A9, FUNCT_1:def 8; :: thesis: verum