let x be FinSequence of REAL ; :: thesis: for A being Matrix of REAL st width A = len x & len x > 0 & len A > 0 holds
len (A * x) = len A
let A be Matrix of REAL ; :: thesis: ( width A = len x & len x > 0 & len A > 0 implies len (A * x) = len A )
assume A1: ( width A = len x & len x > 0 & len A > 0 ) ; :: thesis: len (A * x) = len A
then A2: len (ColVec2Mx x) = len x by Def9;
len (Col (A * (ColVec2Mx x)),1) = len (A * (ColVec2Mx x)) by MATRIX_1:def 9
.= len A by A1, A2, MATRIX_3:def 4 ;
hence len (A * x) = len A ; :: thesis: verum