theorem :: LMOD_XX1:27

for R being comRing
for M being LeftMod of R holds Hom (R,(LeftModule R),M) ~= M