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)

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

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

len (a * (b * M)) = len M
by A2, MATRIX_3:def 5;
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;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

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