theorem Th95: :: MATRIXR2:95

for n being Nat
for x being FinSequence of REAL
for A being Matrix of n,REAL st n > 0 & len x = n holds
x * (A @) = A * x