theorem :: MATRIXR1:12

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:40;