theorem :: VECTSP_1:31

for F being non empty right_complementable add-associative right_zeroed addLoopStr
for a, b being Element of F holds a + b = - ((- b) + (- a))