for F1, F2, F3 being FinSequence of REAL st len F1 = len F2 & len F2 = len F3 holds
(F1 - F2) - F3 = F1 - (F2 + F3) by RVSUM_1:39;