theorem Th16: :: JORDAN23:16

for f being FinSequence st f is one-to-one holds
f is weakly-one-to-one