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 DomL of F, the CodL of F, the Fun of F #) = LModMorphismStr(# G,H,f #) & f is additive & f is homogeneous )