let p be FinSequence; :: thesis: ( ( for n, m being 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 Nat st 1 <= n & n < m & m <= len p holds
p . n <> p . m )

assume A1: for n, m being 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 object ; :: according to FUNCT_1:def 4 :: thesis: ( not x1 in dom p or not x2 in dom p or not p . x1 = p . x2 or x1 = x2 )
assume that
A2: ( x1 in dom p & x2 in dom p ) and
A3: p . x1 = p . x2 ; :: thesis: x1 = x2
reconsider n = x1, m = x2 as Element of NAT by A2;
A4: ( n <= len p & 1 <= m ) by A2, FINSEQ_3:25;
A5: ( 1 <= n & m <= len p ) by A2, FINSEQ_3:25;
assume A6: x1 <> x2 ; :: thesis: contradiction

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

suppose m <= n ; :: thesis: contradiction

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

end;

suppose m > n ; :: thesis: contradiction

hence contradiction by A1, A3, A5; :: thesis: verum

end;

end;

end;

end;

assume A7: p is one-to-one ; :: thesis: for n, m being Nat st 1 <= n & n < m & m <= len p holds
p . n <> p . m
let n, m be Nat; :: thesis: ( 1 <= n & n < m & m <= len p implies p . n <> p . m )
assume that
A8: 1 <= n and
A9: n < m and
A10: m <= len p ; :: thesis: p . n <> p . m
n <= len p by A9, A10, XXREAL_0:2;
then A11: n in dom p by A8, FINSEQ_3:25;
1 <= m by A8, A9, XXREAL_0:2;
then A12: m in dom p by A10, FINSEQ_3:25;
assume p . n = p . m ; :: thesis: contradiction
hence contradiction by A7, A9, A11, A12; :: thesis: verum