let f be FinSequence; :: thesis: ( len f <> 2 implies ( f is weakly-one-to-one iff f is poorly-one-to-one ) )
assume A1: len f <> 2 ; :: thesis: ( f is weakly-one-to-one iff f is poorly-one-to-one )
thus ( f is weakly-one-to-one implies f is poorly-one-to-one ) :: thesis: ( f is poorly-one-to-one implies f is weakly-one-to-one )

proof

assume f is weakly-one-to-one ; :: thesis: f is poorly-one-to-one
then for i being Element of NAT st 1 <= i & i < len f holds
f . i <> f . (i + 1) by Def2;
hence f is poorly-one-to-one by A1, Def3; :: thesis: verum

end;

assume f is poorly-one-to-one ; :: thesis: f is weakly-one-to-one
then for i being Element of NAT st 1 <= i & i < len f holds
f . i <> f . (i + 1) by A1, Def3;
hence f is weakly-one-to-one by Def2; :: thesis: verum