let K be Field; :: thesis: for a being Element of K
for A, B being Matrix of K st width A = len B holds
(a * A) * B = a * (A * B)
let a be Element of K; :: thesis: for A, B being Matrix of K st width A = len B holds
(a * A) * B = a * (A * B)
let A, B be Matrix of K; :: thesis: ( width A = len B implies (a * A) * B = a * (A * B) )
set aA = a * A;
set AB = A * B;
set aAB = a * (A * B);
assume A1: width A = len B ; :: thesis: (a * A) * B = a * (A * B)
then A2: width (A * B) = width B by MATRIX_3:def 4;
A3: len (a * (A * B)) = len (A * B) by MATRIX_3:def 5;
then A4: len (a * (A * B)) = len A by A1, MATRIX_3:def 4;
A5: width (a * A) = width A by MATRIX_3:def 5;
then A6: ( len (a * A) = len A & len (a * A) = len ((a * A) * B) ) by A1, MATRIX_3:def 4, MATRIX_3:def 5;

A7: now

let i, j be Nat; :: thesis: ( [i,j] in Indices (a * (A * B)) implies (a * (A * B)) * i,j = ((a * A) * B) * i,j )
assume [i,j] in Indices (a * (A * B)) ; :: thesis: (a * (A * B)) * i,j = ((a * A) * B) * i,j
then A8: [i,j] in Indices (A * B) by MATRIXR1:18;
then i in dom (A * B) by ZFMISC_1:106;
then i in Seg (len A) by A3, A4, FINSEQ_1:def 3;
then A9: ( 1 <= i & i <= len A ) by FINSEQ_1:3;
dom (A * B) = Seg (len (A * B)) by FINSEQ_1:def 3
.= dom ((a * A) * B) by A3, A4, A6, FINSEQ_1:def 3 ;
then A10: [i,j] in Indices ((a * A) * B) by A1, A5, A2, A8, MATRIX_3:def 4;
thus (a * (A * B)) * i,j = a * ((A * B) * i,j) by A8, MATRIX_3:def 5
.= a * ((Line A,i) "*" (Col B,j)) by A1, A8, MATRIX_3:def 4
.= Sum (a * (mlt (Line A,i),(Col B,j))) by FVSUM_1:92
.= Sum (mlt (a * (Line A,i)),(Col B,j)) by A1, FVSUM_1:82
.= (Line (a * A),i) "*" (Col B,j) by A9, MATRIXR1:20
.= ((a * A) * B) * i,j by A1, A5, A10, MATRIX_3:def 4 ; :: thesis: verum

end;

( width (a * (A * B)) = width (A * B) & width B = width ((a * A) * B) ) by A1, A5, MATRIX_3:def 4, MATRIX_3:def 5;
hence (a * A) * B = a * (A * B) by A2, A4, A6, A7, MATRIX_1:21; :: thesis: verum