let x be FinSequence of REAL ; :: thesis: for A being Matrix of REAL st len A = len x holds
len (x * A) = width A
let A be Matrix of REAL; :: thesis: ( len A = len x implies len (x * A) = width A )
assume A1: len A = len x ; :: thesis: len (x * A) = width A
A2: width (LineVec2Mx x) = len x by Def10;
len (Line (((LineVec2Mx x) * A),1)) = width (MXF2MXR ((MXR2MXF (LineVec2Mx x)) * (MXR2MXF A))) by MATRIX_0:def 7
.= width A by A1, A2, MATRIX_3:def 4 ;
hence len (x * A) = width A ; :: thesis: verum