theorem :: ZMODUL02:45

for R being Ring
for V being LeftMod of R holds the addF of (LC_Z_Module V) = LCAdd V ;