let V be RealLinearSpace; for a being Real
for v, u, w being VECTOR of V holds a * (Sum <*v,u,w*>) = ((a * v) + (a * u)) + (a * w)
let a be Real; for v, u, w being VECTOR of V holds a * (Sum <*v,u,w*>) = ((a * v) + (a * u)) + (a * w)
let v, u, w be VECTOR of V; a * (Sum <*v,u,w*>) = ((a * v) + (a * u)) + (a * w)
thus a * (Sum <*v,u,w*>) =
a * ((v + u) + w)
by Th46
.=
(a * (v + u)) + (a * w)
by Def5
.=
((a * v) + (a * u)) + (a * w)
by Def5
; verum