:: deftheorem Def26 defines cod GRCAT_1:def 28 :
for V being Group_DOMAIN
for b₂ being Function of (Morphs V),V holds
( b₂ = cod V iff for f being Element of Morphs V holds b₂ . f = cod f );