:: deftheorem Def24 defines fDom COH_SP:def 25 :
for X being set
for b₂ being Function of (MapsT X),(TOL X) holds
( b₂ = fDom X iff for m being Element of MapsT X holds b₂ . m = dom m );