theorem Th31: :: RLAFFIN1:31

for S being non empty addLoopStr holds sum (ZeroLC S) = 0