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 ; :: 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
.= a * (b * (A * (i,j))) by
.= (a * b) * (A * (i,j)) by GROUP_1:def 3
.= ((a * b) * A) * (i,j) by ; :: 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 ; :: thesis: verum