theorem :: LMOD_XX1:38

for R being comRing
for M being strict LeftMod of R holds AbGrLMod ((AbGr M),(canHom M)) = M