let R be Ring; 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; 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; 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; (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
; verum