theorem Th5: :: JORDAN23:5

for D being set
for f being FinSequence of D holds
( f is weakly-one-to-one iff for i being Nat st 1 <= i & i < len f holds
f /. i <> f /. (i + 1) )