theorem Th48: :: ZMODUL02:48

for V being Z_Module
for L being Linear_Combination of V
for a being Element of INT.Ring holds a * (vector ((LC_Z_Module V),L)) = a * L