theorem :: RLAFFIN1:18
for r being Real
for V being RealLinearSpace
for v being VECTOR of V
for L being Linear_Combination of V holds v + (r * L) = r * (v + L)