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

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) by VECTSP_1:def 16
.= ((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

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 4
.= ((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_1:21; :: thesis: verum