theorem :: RVSUM_1:15

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