theorem :: RVSUM_2:17

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