theorem :: LMOD_XX1:33

for R being Ring
for M being LeftMod of R
for a being Element of R
for m being Element of M holds ((curry the lmult of M) . a) . m = a * m by LOPBAN_8:7;