theorem :: RVSUM_1:31

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