theorem Th8: :: RVSUM_2:8

for i being Nat
for c being Complex holds - (i |-> c) = i |-> (- c)