:: deftheorem Def3 defines poorly-one-to-one JORDAN23:def 3 :
for f being FinSequence holds
( ( len f <> 2 implies ( f is poorly-one-to-one iff for i being Nat st 1 <= i & i < len f holds
f . i <> f . (i + 1) ) ) & ( not len f <> 2 implies ( f is poorly-one-to-one iff verum ) ) );