theorem Th31: :: ZMODUL02:31

for V being Z_Module
for L being Linear_Combination of V
for a being Element of INT.Ring
for A being Subset of V st L is Linear_Combination of A holds
a * L is Linear_Combination of A by VECTSP_6:31;