theorem Th88: :: RVSUM_1:88

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