theorem :: RVSUM_1:36

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