:: deftheorem defines bijective FUNCT_2:def 4 :
for X, Y being set
for f being b₁ -defined b₂ -valued Function holds
( f is bijective iff ( f is one-to-one & f is onto ) );