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 ;
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 ;
A7: now :: thesis: for i, j being Nat st [i,j] in Indices (a * (A * B)) holds
(a * (A * B)) * (i,j) = ((a * A) * B) * (i,j)
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:87;
then i in Seg (len A) by ;
then A9: ( 1 <= i & i <= len A ) by FINSEQ_1:1;
dom (A * B) = Seg (len (A * B)) by FINSEQ_1:def 3
.= dom ((a * A) * B) by ;
then A10: [i,j] in Indices ((a * A) * B) by ;
thus (a * (A * B)) * (i,j) = a * ((A * B) * (i,j)) by
.= a * ((Line (A,i)) "*" (Col (B,j))) by
.= Sum (a * (mlt ((Line (A,i)),(Col (B,j))))) by FVSUM_1:73
.= Sum (mlt ((a * (Line (A,i))),(Col (B,j)))) by
.= (Line ((a * A),i)) "*" (Col (B,j)) by
.= ((a * A) * B) * (i,j) by ; :: thesis: verum
end;
( width (a * (A * B)) = width (A * B) & width B = width ((a * A) * B) ) by ;
hence (a * A) * B = a * (A * B) by ; :: thesis: verum