theorem :: RLVECT_1:85

for V being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for v, w being Element of V holds
( Sum <*(- v),(- w)*> = - (v + w) & Sum <*(- w),(- v)*> = - (v + w) )