theorem Th58: :: MATRIXR2:58

for x being FinSequence of REAL
for A being Matrix of REAL st width A = len x & len x > 0 & len A > 0 holds
A * (ColVec2Mx x) = ColVec2Mx (A * x)