theorem :: FVSUM_1:75

for K being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for p being FinSequence of the carrier of K holds Sum (- p) = - (Sum p)