theorem Th8: :: FINSEQ_4:8

for f being Function holds
( f is one-to-one iff for y being object st y in rng f holds
f just_once_values y )