for D being non empty set
for G, H being AddGroup holds
( D is GroupMorphism_DOMAIN of G,H iff for x being Element of D holds x is strict Morphism of G,H )