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