:: deftheorem Def1 defines doms FUNCT_6:def 2 :
for f being Function-yielding Function
for b₂ being Function holds
( b₂ = doms f iff ( dom b₂ = dom f & ( for x being object st x in dom f holds
b₂ . x = proj1 (f . x) ) ) );