:: deftheorem Def25 defines dom GRCAT_1:def 27 :
for V being Group_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 );