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 A1: ( len A > 0 & width A > 0 & ( len A = len x or width (A @ ) = len x ) ) ; :: thesis: (A @ ) * x = x * A
then A2: len A = width (A @ ) by MATRIX_2:12;
A3: len A = len x by A1, MATRIX_2:12;
A4: width (LineVec2Mx x) = len x by Def10;
then A5: width (LineVec2Mx x) = len A by A1, MATRIX_2:12;
A6: len (LineVec2Mx x) = 1 by Def10;
A7: width (ColVec2Mx x) = 1 by A1, A2, Def9;
len (ColVec2Mx x) = len x by A1, A2, Def9;
then A8: width ((A @ ) * (ColVec2Mx x)) = width (ColVec2Mx x) by A1, A2, MATRIX_3:def 4;
A9: len ((LineVec2Mx x) * A) = len (LineVec2Mx x) by A5, MATRIX_3:def 4;
A10: width ((LineVec2Mx x) * A) = width A by A5, MATRIX_3:def 4;
A11: 1 in Seg (width ((A @ ) * (ColVec2Mx x))) by A7, A8, FINSEQ_1:3;
Line ((LineVec2Mx x) * A),1 = Line ((((LineVec2Mx x) * A) @ ) @ ),1 by A1, A6, A9, A10, MATRIX_2:15
.= Line (((A @ ) * ((LineVec2Mx x) @ )) @ ),1 by A1, A3, A4, MATRIX_3:24
.= Line (((A @ ) * (ColVec2Mx x)) @ ),1 by A1, A3, Th49
.= Col ((A @ ) * (ColVec2Mx x)),1 by A11, MATRIX_2:17 ;
hence (A @ ) * x = x * A ; :: thesis: verum