:: deftheorem Def19 defines dom RINGCAT1:def 20 :
for V being Ring_DOMAIN
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 );