let R be Ring; :: thesis: for V being RightMod of R holds Sum (ZeroLC V) = 0. V
let V be RightMod of R; :: thesis: Sum (ZeroLC V) = 0. V
consider F being FinSequence of V such that
F is one-to-one and
A1: rng F = Carrier (ZeroLC V) and
A2: Sum (ZeroLC V) = Sum ((ZeroLC V) (#) F) by Def7;
Carrier (ZeroLC V) = {} by Def4;
then F = {} by A1, RELAT_1:41;
then len F = 0 ;
then len ((ZeroLC V) (#) F) = 0 by Def6;
hence Sum (ZeroLC V) = 0. V by A2, RLVECT_1:75; :: thesis: verum