:: deftheorem Def2 defines " FUNCT_3:def 2 :
for f, b₂ being Function holds
( b₂ = " f iff ( dom b₂ = bool (rng f) & ( for Y being set st Y c= rng f holds
b₂ . Y = f " Y ) ) );