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