for G, H being AddGroup
for f being strict GroupMorphismStr st dom f = G & cod f = H & fun f is additive holds
f is strict Morphism of G,H