theorem :: VECTSP_1:33

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