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