theorem :: MATRIXR1:13

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