let R be Ring; :: thesis: for V being RightMod of R
for a being Scalar of R holds (Sum (<*> the carrier of V)) * a = 0. V
let V be RightMod of R; :: thesis: for a being Scalar of R holds (Sum (<*> the carrier of V)) * a = 0. V
let a be Scalar of R; :: thesis: (Sum (<*> the carrier of V)) * a = 0. V
thus (Sum (<*> the carrier of V)) * a = (0. V) * a by RLVECT_1:43
.= 0. V by VECTSP_2:32 ; :: thesis: verum