let R be Ring; :: thesis: for V being RightMod of R
for a being Scalar of R
for u, v, w being Vector of V holds (Sum <*v,u,w*>) * a = ((v * a) + (u * a)) + (w * a)
let V be RightMod of R; :: thesis: for a being Scalar of R
for u, v, w being Vector of V holds (Sum <*v,u,w*>) * a = ((v * a) + (u * a)) + (w * a)
let a be Scalar of R; :: thesis: for u, v, w being Vector of V holds (Sum <*v,u,w*>) * a = ((v * a) + (u * a)) + (w * a)
let u, v, w be Vector of V; :: thesis: (Sum <*v,u,w*>) * a = ((v * a) + (u * a)) + (w * a)
thus (Sum <*v,u,w*>) * a = ((v + u) + w) * a by RLVECT_1:46
.= ((v + u) * a) + (w * a) by VECTSP_2:def 9
.= ((v * a) + (u * a)) + (w * a) by VECTSP_2:def 9 ; :: thesis: verum