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:60;
hence Sum ({} V) = 0. V by Def3, RELAT_1:60; :: thesis: verum