theorem :: MATRIXR2:55

for x being FinSequence of REAL
for A, B being Matrix of REAL st len x = width A & len A = len B & width A = width B & len x > 0 & len A > 0 holds
(A - B) * x = (A * x) - (B * x)