:: deftheorem Def20 defines cod RINGCAT1:def 21 :
for V being Ring_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 );