theorem Th35: :: LMOD_XX1:37

for R being comRing
for M being LeftMod of R holds LModlmult ((AbGr M),(canHom M)) = the lmult of M