:: deftheorem Def12 defines cod MODCAT_1:def 12 :
for R being Ring
for V being LeftMod_DOMAIN of R
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 );