theorem Th7: :: MOD_2:7

for R being Ring
for G, H being LeftMod of R
for F being Morphism of G,H ex f being Function of G,H st
( LModMorphismStr(# the Dom of F, the Cod of F, the Fun of F #) = LModMorphismStr(# G,H,f #) & f is additive & f is homogeneous )