theorem Th34: :: ZMODUL02:34

for V being Z_Module
for L being Linear_Combination of V
for a, b being Element of INT.Ring holds a * (b * L) = (a * b) * L by VECTSP_6:34;