let x be FinSequence of REAL ; 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; ( 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 )
; (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
; verum