let a be Real; :: thesis: 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 ; :: thesis: 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 ; :: thesis: ( len A = len x & len x > 0 & width A > 0 implies (a * x) * A = a * (x * A) )
assume A1: ( len A = len x & len x > 0 & width A > 0 ) ; :: thesis: (a * x) * A = a * (x * A)
then A2: ( width (A @ ) = len x & len x > 0 & len (A @ ) > 0 ) by MATRIX_2:12;
then A3: (A @ ) * (a * x) = a * ((A @ ) * x) by Th59;
A4: (A @ ) * x = x * A by A1, Th52;
len (a * x) = len x by EUCLID_2:8;
then (a * x) * ((A @ ) @ ) = (A @ ) * (a * x) by A2, Th53;
hence (a * x) * A = a * (x * A) by A1, A3, A4, MATRIX_2:15; :: thesis: verum