theorem Th31: :: RLAFFIN1:31
for S being non empty addLoopStr holds sum (ZeroLC S) = 0