let K be Field; :: thesis: for a, b being Element of K
for M being Matrix of K holds a * (b * M) = (a * b) * M
let a, b be Element of K; :: thesis: for M being Matrix of K holds a * (b * M) = (a * b) * M
let M be Matrix of K; :: thesis: a * (b * M) = (a * b) * M
A1: ( len ((a * b) * M) = len M & width ((a * b) * M) = width M ) by MATRIX_3:def 5;
A2: len (a * (b * M)) = len (b * M) by MATRIX_3:def 5;
A3: width (a * (b * M)) = width (b * M) by MATRIX_3:def 5;
then A4: width (a * (b * M)) = width M by MATRIX_3:def 5;
A5: ( len (b * M) = len M & width (b * M) = width M ) by MATRIX_3:def 5;
A6: for i, j being Nat st [i,j] in Indices (a * (b * M)) holds
(a * (b * M)) * (i,j) = ((a * b) * M) * (i,j)

proof

let i, j be Nat; :: thesis: ( [i,j] in Indices (a * (b * M)) implies (a * (b * M)) * (i,j) = ((a * b) * M) * (i,j) )
assume A7: [i,j] in Indices (a * (b * M)) ; :: thesis: (a * (b * M)) * (i,j) = ((a * b) * M) * (i,j)
A8: Indices (b * M) = Indices M by A5, MATRIX_4:55;
A9: Indices (a * (b * M)) = Indices (b * M) by A2, A3, MATRIX_4:55;
then (a * (b * M)) * (i,j) = a * ((b * M) * (i,j)) by A7, MATRIX_3:def 5
.= a * (b * (M * (i,j))) by A7, A9, A8, MATRIX_3:def 5
.= (a * b) * (M * (i,j)) by GROUP_1:def 3 ;
hence (a * (b * M)) * (i,j) = ((a * b) * M) * (i,j) by A7, A9, A8, MATRIX_3:def 5; :: thesis: verum

end;

len (a * (b * M)) = len M by A2, MATRIX_3:def 5;
hence a * (b * M) = (a * b) * M by A1, A4, A6, MATRIX_0:21; :: thesis: verum