theorem Th73: :: FUNCT_1:74

for f being Function holds
( ( for y being object st y in rng f holds
ex x being object st f " {y} = {x} ) iff f is one-to-one )