theorem :: VECTSP_7:22

for R being Ring
for V being LeftMod of R
for L being Linear_Combination of V
for a being Scalar of holds Sum (a * L) = a * (Sum L) by TH3;