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 ;
A9: Indices (a * (b * M)) = Indices (b * M) by ;
then (a * (b * M)) * (i,j) = a * ((b * M) * (i,j)) by
.= a * (b * (M * (i,j))) by
.= (a * b) * (M * (i,j)) by GROUP_1:def 3 ;
hence (a * (b * M)) * (i,j) = ((a * b) * M) * (i,j) by ; :: thesis: verum
end;
len (a * (b * M)) = len M by ;
hence a * (b * M) = (a * b) * M by ; :: thesis: verum