theorem :: RLVECT_1:50

for V being non empty right_complementable add-associative right_zeroed addLoopStr holds - (Sum (<*> the carrier of V)) = 0. V