theorem Th40: :: RLAFFIN1:40

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