:: deftheorem Def17 defines GroupMorphism_DOMAIN GRCAT_1:def 19 :
for G, H being AddGroup
for b₃ being GroupMorphism_DOMAIN holds
( b₃ is GroupMorphism_DOMAIN of G,H iff for x being Element of b₃ holds x is strict Morphism of G,H );