for G, H being AddGroup
for f being strict Morphism of G,H holds {f} is GroupMorphism_DOMAIN of G,H