let f be FinSequence; :: thesis: ( f is almost-one-to-one implies f is poorly-one-to-one )
assume A1: f is almost-one-to-one ; :: thesis: f is poorly-one-to-one

per cases ( len f <> 2 or len f = 2 ) ;
:: according to JORDAN23:def 3

case A2: len f <> 2 ; :: thesis: for i being Nat st 1 <= i & i < len f holds
f . i <> f . (i + 1)

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

per cases ( len f <> 0 or len f = 0 ) ;

suppose A3: len f <> 0 ; :: 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) )
A4: ( not i = len f or not i + 1 = 1 ) by A3;
A5: i + 1 >= 1 by NAT_1:11;
assume that
A6: 1 <= i and
A7: i < len f ; :: thesis: f . i <> f . (i + 1)
i + 1 <= len f by A7, NAT_1:13;
then A8: i + 1 in dom f by A5, FINSEQ_3:25;
A9: ( not i = 1 or not i + 1 = len f ) by A2;
A10: i <> i + 1 ;
i in dom f by A6, A7, FINSEQ_3:25;
hence f . i <> f . (i + 1) by A1, A8, A10, A9, A4; :: thesis: verum

end;

suppose A11: len f = 0 ; :: 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
A12: 1 <= i and
A13: i < len f ; :: thesis: f . i <> f . (i + 1)
thus f . i <> f . (i + 1) by A11, A12, A13; :: thesis: verum

end;

end;

end;

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

end;

case len f = 2 ; :: thesis: verum

end;

end;