let S be non empty addLoopStr ; :: thesis: sum (ZeroLC S) = 0

consider F being FinSequence of S such that

F is one-to-one and

A1: rng F = Carrier (ZeroLC S) and

A2: sum (ZeroLC S) = Sum ((ZeroLC S) * F) by Def3;

F = {} by A1, RLVECT_2:def 5;

hence sum (ZeroLC S) = 0 by A2, RVSUM_1:72; :: thesis: verum

consider F being FinSequence of S such that

F is one-to-one and

A1: rng F = Carrier (ZeroLC S) and

A2: sum (ZeroLC S) = Sum ((ZeroLC S) * F) by Def3;

F = {} by A1, RLVECT_2:def 5;

hence sum (ZeroLC S) = 0 by A2, RVSUM_1:72; :: thesis: verum