for X being non empty right_zeroed addLoopStr
for V1, V2 being Subset of X st 0. X in V2 holds
V1 c= V1 + V2