theorem :: MATRIXR1:4

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