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