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 that

A1: len A = len x and

A2: len x > 0 and

A3: width A > 0 ; :: thesis: (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; :: thesis: verum

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 that

A1: len A = len x and

A2: len x > 0 and

A3: width A > 0 ; :: thesis: (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; :: thesis: verum