let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; :: thesis: for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr of 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 VectSpStr of GF; :: thesis: Sum (ZeroLC V) = 0. V
consider F being FinSequence of the carrier 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 Def9;
Carrier (ZeroLC V) = {} by Def6;
then F = {} by A1, RELAT_1:64;
then len F = 0 ;
then len ((ZeroLC V) (#) F) = 0 by Def8;
hence Sum (ZeroLC V) = 0. V by A2, RLVECT_1:94; :: thesis: verum