theorem :: MATRIXR2:48

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