theorem :: MATRIXR1:58
for x1, x2 being FinSequence of REAL
for A being Matrix of REAL st len x1 = len x2 & len A = len x1 holds
(x1 + x2) * A = (x1 * A) + (x2 * A)