theorem Th39: :: RVSUM_2:39

for F being complex-valued FinSequence holds Sum (- F) = - (Sum F)