for V being non empty right_complementable add-associative right_zeroed addLoopStr
for v being Element of V holds (0. V) - v = - v ;