theorem Th32: :: ZMODUL02:32
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 * L) + (b * L) by VECTSP_6:32;