let R be Ring; :: thesis: for V being RightMod of R holds Sum ({} V) = 0. V
let V be RightMod of R; :: thesis: Sum ({} V) = 0. V
Sum (<*> the carrier of V) = 0. V by RLVECT_1:43;
hence Sum ({} V) = 0. V by Def1, RELAT_1:38; :: thesis: verum