theorem :: RVSUM_1:35

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