:: deftheorem Def11 defines GroupMorphism-like GRCAT_1:def 13 :
for IT being GroupMorphismStr holds
( IT is GroupMorphism-like iff fun IT is additive );