:: deftheorem Def1 defines .: FUNCT_3:def 1 :
for f, b₂ being Function holds
( b₂ = .: f iff ( dom b₂ = bool (dom f) & ( for X being set st X c= dom f holds
b₂ . X = f .: X ) ) );