theorem :: RLVECT_1:80

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