:: deftheorem defines cod RINGCAT1:def 3 :
for f being RingMorphismStr holds cod f = the CodR of f;