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