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)

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

hence
v + (r * L) = r * (v + L)
; :: thesis: verumlet 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;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