theorem :: RLVECT_1:82

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