theorem Th64: :: MATRIXR1:64
for x being FinSequence of REAL
for A, B being Matrix of REAL st len A = len B & width A = width B & len A = len x holds
x * (A + B) = (x * A) + (x * B)