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 (b * M) = len M & width (b * M) = width M ) by MATRIX_3:def 5;
A2: ( len ((a * b) * M) = len M & width ((a * b) * M) = width M ) by MATRIX_3:def 5;
A3: len (a * (b * M)) = len (b * M) by MATRIX_3:def 5;
then A4: len (a * (b * M)) = len M by MATRIX_3:def 5;
A5: width (a * (b * M)) = width (b * M) by MATRIX_3:def 5;
then A6: width (a * (b * M)) = width M by MATRIX_3:def 5;
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 (a * (b * M)) = Indices (b * M) by A3, A5, MATRIX_4:55;
A9: Indices (b * M) = Indices M by A1, MATRIX_4:55;
(a * (b * M)) * i,j = a * ((b * M) * i,j) by A7, A8, MATRIX_3:def 5
.= a * (b * (M * i,j)) by A7, A8, A9, MATRIX_3:def 5
.= (a * b) * (M * i,j) by GROUP_1:def 4 ;
hence (a * (b * M)) * i,j = ((a * b) * M) * i,j by A7, A8, A9, MATRIX_3:def 5; :: thesis: verum

end;

hence a * (b * M) = (a * b) * M by A2, A4, A6, MATRIX_1:21; :: thesis: verum