theorem :: MATRIXR1:57

for x1, x2 being FinSequence of REAL
for A being Matrix of REAL st len x1 = len x2 & width A = len x1 & len x1 > 0 holds
A * (x1 + x2) = (A * x1) + (A * x2)