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