theorem :: RVSUM_1:39

for F1, F2, F3 being real-valued FinSequence holds (F1 - F2) - F3 = F1 - (F2 + F3) by RFUNCT_1:20;