for R being Ring
for G, H being LeftMod of R
for f being LModMorphismStr over R st dom f = G & cod f = H & fun f is additive & fun f is homogeneous holds
f is Morphism of G,H