:: deftheorem defines cod GRCAT_1:def 10 :
for f being GroupMorphismStr holds cod f = the Target of f;