:: deftheorem Def11 defines dom MODCAT_1:def 11 :
for R being Ring
for V being LeftMod_DOMAIN of R
for b₃ being Function of (Morphs V),V holds
( b₃ = dom V iff for f being Element of Morphs V holds b₃ . f = dom' f );