theorem Th32: :: ZMODUL02:32

for R being Ring
for V being LeftMod of R
for L being Linear_Combination of V
for a, b being Element of R holds (a + b) * L = (a * L) + (b * L) by VECTSP_6:32;