let V be RealLinearSpace; :: 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 Def8;

Carrier (ZeroLC V) = {} by Def5;

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

then len F = 0 ;

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

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

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 Def8;

Carrier (ZeroLC V) = {} by Def5;

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

then len F = 0 ;

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

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