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 C = a * B;
set D = a * (A * B);
A1: len (a * (A * B)) = len (A * B) by MATRIX_3:def 5;
assume A2: width A = len B ; :: thesis: A * (a * B) = a * (A * B)
then width (A * B) = width B by MATRIX_3:def 4;
then A3: width (a * (A * B)) = width B by MATRIX_3:def 5
.= width (a * B) by MATRIX_3:def 5 ;
A4: width B = width (a * B) by MATRIX_3:def 5;
A5: 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)) )
reconsider xo = Col (B,j) as Element of (width A) -tuples_on the carrier of K by A2;
assume A6: [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 A4, A3, ZFMISC_1:87;
then A7: ( 1 <= j & j <= width B ) by FINSEQ_1:1;
dom (A * B) = dom (a * (A * B)) by A1, FINSEQ_3:29;
then A8: [i,j] in Indices (A * B) by A6, MATRIX_3:def 5;
then (a * (A * B)) * (i,j) = a * ((A * B) * (i,j)) by MATRIX_3:def 5;
then (a * (A * B)) * (i,j) = a * ((Line (A,i)) "*" (Col (B,j))) by A2, A8, MATRIX_3:def 4
.= a * (Sum (mlt ((Line (A,i)),(Col (B,j))))) by FVSUM_1:def 9
.= Sum (a * (mlt ((Line (A,i)),(Col (B,j))))) by FVSUM_1:73
.= Sum (mlt ((Line (A,i)),(a * xo))) by FVSUM_1:69
.= Sum (mlt ((Line (A,i)),(Col ((a * B),j)))) by A7, Th19 ;
hence (a * (A * B)) * (i,j) = (Line (A,i)) "*" (Col ((a * B),j)) by FVSUM_1:def 9; :: thesis: verum

end;

( len (a * B) = len B & len (A * B) = len A ) by A2, MATRIX_3:def 4, MATRIX_3:def 5;
hence A * (a * B) = a * (A * B) by A2, A1, A3, A5, MATRIX_3:def 4; :: thesis: verum