theorem :: VECTSP_1:16

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