let D be set ; :: thesis: for f being FinSequence of D holds
( f is weakly-one-to-one iff for i being Nat st 1 <= i & i < len f holds
f /. i <> f /. (i + 1) )
let f be FinSequence of D; :: thesis: ( f is weakly-one-to-one iff for i being Nat st 1 <= i & i < len f holds
f /. i <> f /. (i + 1) )
thus ( f is weakly-one-to-one implies for i being Nat st 1 <= i & i < len f holds
f /. i <> f /. (i + 1) ) :: thesis: ( ( for i being Nat st 1 <= i & i < len f holds
f /. i <> f /. (i + 1) ) implies f is weakly-one-to-one )

proof

assume A1: f is weakly-one-to-one ; :: thesis: for i being Nat st 1 <= i & i < len f holds
f /. i <> f /. (i + 1)
let i be Nat; :: thesis: ( 1 <= i & i < len f implies f /. i <> f /. (i + 1) )
assume that
A2: 1 <= i and
A3: i < len f ; :: thesis: f /. i <> f /. (i + 1)
A4: i + 1 <= len f by A3, NAT_1:13;
1 < i + 1 by A2, NAT_1:13;
then A5: f . (i + 1) = f /. (i + 1) by A4, FINSEQ_4:15;
f . i = f /. i by A2, A3, FINSEQ_4:15;
hence f /. i <> f /. (i + 1) by A1, A2, A3, A5; :: thesis: verum

end;

assume A6: for i being Nat st 1 <= i & i < len f holds
f /. i <> f /. (i + 1) ; :: thesis: f is weakly-one-to-one

now :: thesis: for i being Nat st 1 <= i & i < len f holds
f . i <> f . (i + 1)

let i be Nat; :: thesis: ( 1 <= i & i < len f implies f . i <> f . (i + 1) )
assume that
A7: 1 <= i and
A8: i < len f ; :: thesis: f . i <> f . (i + 1)
A9: i + 1 <= len f by A8, NAT_1:13;
1 < i + 1 by A7, NAT_1:13;
then A10: f . (i + 1) = f /. (i + 1) by A9, FINSEQ_4:15;
f . i = f /. i by A7, A8, FINSEQ_4:15;
hence f . i <> f . (i + 1) by A6, A7, A8, A10; :: thesis: verum

end;

hence f is weakly-one-to-one ; :: thesis: verum