:: deftheorem Def3 defines onto FUNCT_2:def 3 :
for Y being set
for f being b₁ -valued Relation holds
( f is onto iff rng f = Y );