let K be Field; :: thesis: for a, b being Element of K
for A being Matrix of K holds
( (1_ K) * A = A & a * (b * A) = (a * b) * A )
let a, b be Element of K; :: thesis: for A being Matrix of K holds
( (1_ K) * A = A & a * (b * A) = (a * b) * A )
let A be Matrix of K; :: thesis: ( (1_ K) * A = A & a * (b * A) = (a * b) * A )
set 1A = (1_ K) * A;
set bA = b * A;
set ab = a * b;
set abA = (a * b) * A;

A1: now :: thesis: for i, j being Nat st [i,j] in Indices A holds
A * (i,j) = ((1_ K) * A) * (i,j)

let i, j be Nat; :: thesis: ( [i,j] in Indices A implies A * (i,j) = ((1_ K) * A) * (i,j) )
assume A2: [i,j] in Indices A ; :: thesis: A * (i,j) = ((1_ K) * A) * (i,j)
thus A * (i,j) = (1_ K) * (A * (i,j))
.= ((1_ K) * A) * (i,j) by A2, MATRIX_3:def 5 ; :: thesis: verum

end;

A3: len (a * (b * A)) = len (b * A) by MATRIX_3:def 5
.= len A by MATRIX_3:def 5
.= len ((a * b) * A) by MATRIX_3:def 5 ;

A4: now :: thesis: for i, j being Nat st [i,j] in Indices (a * (b * A)) holds
(a * (b * A)) * (i,j) = ((a * b) * A) * (i,j)

A5: Indices (b * A) = Indices A by MATRIXR1:18;
A6: Indices (a * (b * A)) = Indices (b * A) by MATRIXR1:18;
let i, j be Nat; :: thesis: ( [i,j] in Indices (a * (b * A)) implies (a * (b * A)) * (i,j) = ((a * b) * A) * (i,j) )
assume A7: [i,j] in Indices (a * (b * A)) ; :: thesis: (a * (b * A)) * (i,j) = ((a * b) * A) * (i,j)
thus (a * (b * A)) * (i,j) = a * ((b * A) * (i,j)) by A7, A6, MATRIX_3:def 5
.= a * (b * (A * (i,j))) by A7, A6, A5, MATRIX_3:def 5
.= (a * b) * (A * (i,j)) by GROUP_1:def 3
.= ((a * b) * A) * (i,j) by A7, A6, A5, MATRIX_3:def 5 ; :: thesis: verum

end;

A8: width (a * (b * A)) = width (b * A) by MATRIX_3:def 5
.= width A by MATRIX_3:def 5
.= width ((a * b) * A) by MATRIX_3:def 5 ;
( len ((1_ K) * A) = len A & width ((1_ K) * A) = width A ) by MATRIX_3:def 5;
hence ( (1_ K) * A = A & a * (b * A) = (a * b) * A ) by A1, A3, A8, A4, MATRIX_0:21; :: thesis: verum