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 )