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) )
assume A1: width A = len B ; :: thesis: A * (a * B) = a * (A * B)
set C = a * B;
set D = a * (A * B);
A2: len (a * (A * B)) = len (A * B) by MATRIX_3:def 5;
A3: len (a * B) = len B by MATRIX_3:def 5;
A4: len (A * B) = len A by A1, MATRIX_3:def 4;
A5: width (A * B) = width B by A1, MATRIX_3:def 4;
A6: width B = width (a * B) by MATRIX_3:def 5;
A7: width (a * (A * B)) = width B by A5, MATRIX_3:def 5
.= width (a * B) by MATRIX_3:def 5 ;
for i, j being Nat st [i,j] in Indices (a * (A * B)) holds
(a * (A * B)) * i,j = (Line A,i) "*" (Col (a * B),j)

proof

let i, j be Nat; :: thesis: ( [i,j] in Indices (a * (A * B)) implies (a * (A * B)) * i,j = (Line A,i) "*" (Col (a * B),j) )
assume A8: [i,j] in Indices (a * (A * B)) ; :: thesis: (a * (A * B)) * i,j = (Line A,i) "*" (Col (a * B),j)
then j in Seg (width B) by A6, A7, ZFMISC_1:106;
then A9: ( 1 <= j & j <= width B ) by FINSEQ_1:3;
dom (A * B) = dom (a * (A * B)) by A2, FINSEQ_3:31;
then A10: [i,j] in Indices (A * B) by A8, MATRIX_3:def 5;
then A11: (a * (A * B)) * i,j = a * ((A * B) * i,j) by MATRIX_3:def 5;
reconsider xo = Col B,j as Element of (width A) -tuples_on the carrier of K by A1;
(a * (A * B)) * i,j = a * ((Line A,i) "*" (Col B,j)) by A1, A10, A11, MATRIX_3:def 4
.= a * (Sum (mlt (Line A,i),(Col B,j))) by FVSUM_1:def 10
.= Sum (a * (mlt (Line A,i),(Col B,j))) by FVSUM_1:92
.= Sum (mlt (Line A,i),(a * xo)) by FVSUM_1:83
.= Sum (mlt (Line A,i),(Col (a * B),j)) by A9, Th19 ;
hence (a * (A * B)) * i,j = (Line A,i) "*" (Col (a * B),j) by FVSUM_1:def 10; :: thesis: verum

end;

hence A * (a * B) = a * (A * B) by A1, A2, A3, A4, A7, MATRIX_3:def 4; :: thesis: verum