theorem Th26: :: RVSUM_1:26

for F1, F2 being real-valued FinSequence holds - (F1 + F2) = (- F1) + (- F2)