let R be Ring; :: thesis: for r1, r2 being Element of R
for A being Matrix of R holds r1 * (r2 * A) = (r1 * r2) * A
let r1, r2 be Element of R; :: thesis: for A being Matrix of R holds r1 * (r2 * A) = (r1 * r2) * A
let A be Matrix of R; :: thesis: r1 * (r2 * A) = (r1 * r2) * A
A1: ( len (r1 * (r2 * A)) = len (r2 * A) & len (r2 * A) = len A & len ((r1 * r2) * A) = len A ) by MATRIX_3:def 5;
A2: ( width (r1 * (r2 * A)) = width (r2 * A) & width (r2 * A) = width A & width ((r1 * r2) * A) = width A ) by MATRIX_3:def 5;
for i, j being Nat st [i,j] in Indices (r1 * (r2 * A)) holds
(r1 * (r2 * A)) * (i,j) = ((r1 * r2) * A) * (i,j)

proof

let i, j be Nat; :: thesis: ( [i,j] in Indices (r1 * (r2 * A)) implies (r1 * (r2 * A)) * (i,j) = ((r1 * r2) * A) * (i,j) )
assume A3: [i,j] in Indices (r1 * (r2 * A)) ; :: thesis: (r1 * (r2 * A)) * (i,j) = ((r1 * r2) * A) * (i,j)
A4: Indices A = [:(dom A),(Seg (width A)):] by MATRIX_0:def 4
.= [:(Seg (len A)),(Seg (width A)):] by FINSEQ_1:def 3
.= [:(dom (r2 * A)),(Seg (width (r2 * A))):] by A1, A2, FINSEQ_1:def 3
.= Indices (r2 * A) by MATRIX_0:def 4 ;
A5: Indices A = [:(dom A),(Seg (width A)):] by MATRIX_0:def 4
.= [:(Seg (len A)),(Seg (width A)):] by FINSEQ_1:def 3
.= [:(dom (r1 * (r2 * A))),(Seg (width (r1 * (r2 * A)))):] by A1, A2, FINSEQ_1:def 3
.= Indices (r1 * (r2 * A)) by MATRIX_0:def 4 ;
hence (r1 * (r2 * A)) * (i,j) = r1 * ((r2 * A) * (i,j)) by A3, A4, MATRIX_3:def 5
.= r1 * (r2 * (A * (i,j))) by A3, A5, MATRIX_3:def 5
.= (r1 * r2) * (A * (i,j)) by GROUP_1:def 3
.= ((r1 * r2) * A) * (i,j) by A3, A5, MATRIX_3:def 5 ;
:: thesis: verum

end;

hence r1 * (r2 * A) = (r1 * r2) * A by A1, A2, MATRIX_0:21; :: thesis: verum