theorem Th34: :: FUNCT_6:39

for f being Function-yielding Function st not {} in rng f holds
( Frege f is one-to-one iff for g being Function st g in rng f holds
g is one-to-one )