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: ( len ((1_ K) * A) = len A & width ((1_ K) * A) = width A ) by MATRIX_3:def 5;

A2: now

let i, j be Nat; :: thesis: ( [i,j] in Indices A implies A * i,j = ((1_ K) * A) * i,j )
assume A3: [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 A3, MATRIX_3:def 5 ; :: thesis: verum

end;

A4: 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 ;
A5: 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 ;

now

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 A6: [i,j] in Indices (a * (b * A)) ; :: thesis: (a * (b * A)) * i,j = ((a * b) * A) * i,j
A7: ( Indices (a * (b * A)) = Indices (b * A) & Indices (b * A) = Indices A & Indices A = Indices ((a * b) * A) ) by MATRIXR1:18;
hence (a * (b * A)) * i,j = a * ((b * A) * i,j) by A6, MATRIX_3:def 5
.= a * (b * (A * i,j)) by A6, A7, MATRIX_3:def 5
.= (a * b) * (A * i,j) by GROUP_1:def 4
.= ((a * b) * A) * i,j by A6, A7, MATRIX_3:def 5 ;
:: thesis: verum

end;

hence ( (1_ K) * A = A & a * (b * A) = (a * b) * A ) by A1, A2, A4, A5, MATRIX_1:21; :: thesis: verum