let x be FinSequence of REAL ; :: thesis: for A being Matrix of REAL st len A > 0 & width A > 0 & ( len A = len x or width (A @) = len x ) holds
(A @) * x = x * A
let A be Matrix of REAL; :: thesis: ( len A > 0 & width A > 0 & ( len A = len x or width (A @) = len x ) implies (A @) * x = x * A )
assume that
A1: len A > 0 and
A2: width A > 0 and
A3: ( len A = len x or width (A @) = len x ) ; :: thesis: (A @) * x = x * A
A4: len A = len x by A2, A3, MATRIX_0:54;
A5: len A = width (A @) by A2, MATRIX_0:54;
then len (ColVec2Mx x) = len x by A1, A3, Def9;
then A6: width ((A @) * (ColVec2Mx x)) = width (ColVec2Mx x) by A3, A5, MATRIX_3:def 4;
width (ColVec2Mx x) = 1 by A1, A3, A5, Def9;
then A7: 1 in Seg (width ((A @) * (ColVec2Mx x))) by A6, FINSEQ_1:1;
A8: len (LineVec2Mx x) = 1 by Def10;
A9: width (LineVec2Mx x) = len x by Def10;
then width (LineVec2Mx x) = len A by A2, A3, MATRIX_0:54;
then ( len ((LineVec2Mx x) * A) = len (LineVec2Mx x) & width ((LineVec2Mx x) * A) = width A ) by MATRIX_3:def 4;
then Line (((LineVec2Mx x) * A),1) = Line (((((LineVec2Mx x) * A) @) @),1) by A2, A8, MATRIX_0:57
.= Line ((((A @) * ((LineVec2Mx x) @)) @),1) by A2, A4, A9, MATRIX_3:22
.= Line ((((A @) * (ColVec2Mx x)) @),1) by A1, A4, Th49
.= Col (((A @) * (ColVec2Mx x)),1) by A7, MATRIX_0:59 ;
hence (A @) * x = x * A ; :: thesis: verum