for V being non empty right_complementable add-associative right_zeroed addLoopStr
for v, w being Element of V st ( v + w = v or w + v = v ) holds
w = 0. V