for V being non empty right_zeroed addLoopStr
for M being Subset of V holds M + {(0. V)} = M by Lm9;