theorem :: ZMODUL02:46

for R being Ring
for V being LeftMod of R holds the lmult of (LC_Z_Module V) = LCMult V ;