theorem :: ZMODUL02:44

for R being Ring
for V being LeftMod of R holds 0. (LC_Z_Module V) = ZeroLC V ;