:: deftheorem Def9 defines fDom ENS_1:def 9 :
for V being non empty set
for b₂ being Function of (Maps V),V holds
( b₂ = fDom V iff for m being Element of Maps V holds b₂ . m = dom m );