theorem :: MATRIXR1:15

for F1, F2 being FinSequence of REAL st len F1 = len F2 holds
F1 = (F1 - F2) + F2