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