for V being RealLinearSpace
for a being Real
for L1, L2 being Linear_Combination of V holds a * (L1 + L2) = (a * L1) + (a * L2)