theorem :: ZMODUL02:46

for V being Z_Module holds the lmult of (LC_Z_Module V) = LCMult V ;