let GF be non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr ; :: thesis: for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF holds Sum (ZeroLC V) = 0. V

let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF; :: 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 Def6;

Carrier (ZeroLC V) = {} by Def3;

then F = {} by A1, RELAT_1:41;

then len F = 0 ;

then len ((ZeroLC V) (#) F) = 0 by Def5;

hence Sum (ZeroLC V) = 0. V by A2, RLVECT_1:75; :: thesis: verum

let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF; :: 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 Def6;

Carrier (ZeroLC V) = {} by Def3;

then F = {} by A1, RELAT_1:41;

then len F = 0 ;

then len ((ZeroLC V) (#) F) = 0 by Def5;

hence Sum (ZeroLC V) = 0. V by A2, RLVECT_1:75; :: thesis: verum