theorem Th35: :: RLAFFIN1:35

for r being Real
for V being RealLinearSpace
for L being Linear_Combination of V holds sum (r * L) = r * (sum L)