theorem :: LMOD_XX1:17

for R being Ring
for M, N being LeftMod of R holds Func_Mod (R,M,N) is LeftMod of R ;