for V being non empty addLoopStr holds Sum (<*> the carrier of V) = 0. V by Lm4;