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