theorem Th39: :: RVSUM_2:39
for F being complex-valued FinSequence holds Sum (- F) = - (Sum F)