theorem Th22: :: FVSUM_1:22

for i being Nat
for K being non empty addLoopStr
for a being Element of K
for p being FinSequence of the carrier of K st i in dom (- p) & a = p . i holds
(- p) . i = - a