let r be Real; :: thesis: for V being RealLinearSpace
for v being VECTOR of V
for L being Linear_Combination of V holds v + (r * L) = r * (v + L)
let V be RealLinearSpace; :: thesis: for v being VECTOR of V
for L being Linear_Combination of V holds v + (r * L) = r * (v + L)
let v be VECTOR of V; :: thesis: for L being Linear_Combination of V holds v + (r * L) = r * (v + L)
let L be Linear_Combination of V; :: thesis: v + (r * L) = r * (v + L)

now :: thesis: for w being VECTOR of V holds (v + (r * L)) . w = (r * (v + L)) . w

let w be VECTOR of V; :: thesis: (v + (r * L)) . w = (r * (v + L)) . w
thus (v + (r * L)) . w = (r * L) . (w - v) by Def1
.= r * (L . (w - v)) by RLVECT_2:def 11
.= r * ((v + L) . w) by Def1
.= (r * (v + L)) . w by RLVECT_2:def 11 ; :: thesis: verum

end;

hence v + (r * L) = r * (v + L) ; :: thesis: verum