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

proof

assume that
A1: f is poorly-one-to-one and
A2: len f <> 2 ; :: thesis:
let i be Nat; :: thesis:
assume that
A3: 1 <= i and
A4: i < len f ; :: thesis:
A5: i + 1 <= len f by A4, NAT_1:13;
1 < i + 1 by A3, NAT_1:13;
then A6: f . (i + 1) = f /. (i + 1) by A5, FINSEQ_4:15;
f . i = f /. i by A3, A4, FINSEQ_4:15;
hence f /. i <> f /. (i + 1) by A1, A2, A3, A4, A6, Def3; :: thesis:

end;

assume A7: ( len f <> 2 implies for i being Nat st 1 <= i & i < len f holds
f /. i <> f /. (i + 1) ) ; :: thesis:

per cases ;

suppose A8: len f <> 2 ; :: thesis:

now :: thesis:

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

end;

hence f is poorly-one-to-one by A8, Def3; :: thesis:

end;

suppose len f = 2 ; :: thesis:

hence f is poorly-one-to-one by Def3; :: thesis:

end;

end;