theorem Th25: :: FVSUM_1:25

for i being Nat
for K being non empty addLoopStr
for a being Element of K holds - (i |-> a) = i |-> (- a)