theorem :: RVSUM_1:34

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