theorem Th8: :: RLVECT_2:8

for V being non empty Abelian add-associative right_zeroed addLoopStr holds Sum ({} V) = 0. V