theorem :: ZMODUL02:43

for R being Ring
for V being LeftMod of R holds the carrier of (LC_Z_Module V) = LinComb V ;