theorem Th8: :: FUNCTOR0:8

for f being Function st f is one-to-one holds
~ f is one-to-one