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

proof

assume A1: ( f is poorly-one-to-one & len f <> 2 ) ; :: thesis: for i being Element of NAT st 1 <= i & i < len f holds
f /. i <> f /. (i + 1)
let i be Element of NAT ; :: thesis: ( 1 <= i & i < len f implies f /. i <> f /. (i + 1) )
assume A2: ( 1 <= i & i < len f ) ; :: thesis: f /. i <> f /. (i + 1)
A3: f . i = f /. i by A2, FINSEQ_4:24;
( 1 < i + 1 & i + 1 <= len f ) by A2, NAT_1:13;
then f . (i + 1) = f /. (i + 1) by FINSEQ_4:24;
hence f /. i <> f /. (i + 1) by A1, A2, A3, Def3; :: thesis: verum

end;

assume A4: ( len f <> 2 implies for i being Element of NAT st 1 <= i & i < len f holds
f /. i <> f /. (i + 1) ) ; :: thesis: f is poorly-one-to-one

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

suppose A5: len f <> 2 ; :: thesis: f is poorly-one-to-one

now

let i be Element of NAT ; :: thesis: ( 1 <= i & i < len f implies f . i <> f . (i + 1) )
assume A6: ( 1 <= i & i < len f ) ; :: thesis: f . i <> f . (i + 1)
A7: f . i = f /. i by A6, FINSEQ_4:24;
( 1 < i + 1 & i + 1 <= len f ) by A6, NAT_1:13;
then f . (i + 1) = f /. (i + 1) by FINSEQ_4:24;
hence f . i <> f . (i + 1) by A4, A5, A6, A7; :: thesis: verum

end;

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

end;

suppose len f = 2 ; :: thesis: f is poorly-one-to-one

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

end;

end;