let a be Real; for x being FinSequence of REAL
for A being Matrix of REAL st len A = len x & len x > 0 & width A > 0 holds
(a * x) * A = a * (x * A)
let x be FinSequence of REAL ; for A being Matrix of REAL st len A = len x & len x > 0 & width A > 0 holds
(a * x) * A = a * (x * A)
let A be Matrix of REAL; ( len A = len x & len x > 0 & width A > 0 implies (a * x) * A = a * (x * A) )
assume that
A1:
len A = len x
and
A2:
len x > 0
and
A3:
width A > 0
; (a * x) * A = a * (x * A)
A4:
(A @) * x = x * A
by A1, A2, A3, Th52;
A5:
width (A @) = len x
by A1, A3, MATRIX_0:54;
then A6:
(A @) * (a * x) = a * ((A @) * x)
by A2, Th59;
A7:
len (a * x) = len x
by RVSUM_1:117;
len (A @) > 0
by A3, MATRIX_0:54;
then
(a * x) * ((A @) @) = (A @) * (a * x)
by A2, A5, A7, Th53;
hence
(a * x) * A = a * (x * A)
by A1, A2, A3, A6, A4, MATRIX_0:57; verum