theorem :: ZMODUL02:53

for V being Z_Module
for a being Element of INT.Ring
for L being Linear_Combination of V holds Sum (a * L) = a * (Sum L) by MOD_3:3;