theorem Th63: :: MATRIXR1:63
for x being FinSequence of REAL
for A, B being Matrix of REAL st len A = len B & width A = width B & width A = len x & len x > 0 holds
(A + B) * x = (A * x) + (B * x)