for K being non empty addLoopStr
for R being Element of 0 -tuples_on the carrier of K holds Sum R = 0. K