for V being RealLinearSpace
for a, b being Real
for L being Linear_Combination of V holds (a + b) * L = (a * L) + (b * L)