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

proof

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

proof

A8: dom (r1 * A) = Seg (len (r1 * A)) by FINSEQ_1:def 3
.= Seg (len A) by MATRIX_3:def 5
.= dom A by FINSEQ_1:def 3 ;
[i,j] in [:(dom A),(Seg (width A)):] by A6, MATRIX_0:def 4;
then [i,j] in [:(dom (r1 * A)),(Seg (width (r1 * A))):] by A8, MATRIX_3:def 5;
hence [i,j] in Indices (r1 * A) by MATRIX_0:def 4; :: thesis: verum

end;

A9: [i,j] in Indices (A * r2)

proof

A10: dom (A * r2) = Seg (len (A * r2)) by FINSEQ_1:def 3
.= Seg (len A) by MATRIX_3:def 6
.= dom A by FINSEQ_1:def 3 ;
[i,j] in [:(dom A),(Seg (width A)):] by A6, MATRIX_0:def 4;
then [i,j] in [:(dom (A * r2)),(Seg (width (A * r2))):] by A10, MATRIX_3:def 6;
hence [i,j] in Indices (A * r2) by MATRIX_0:def 4; :: thesis: verum

end;

thus ((r1 * A) * r2) * (i,j) = ((r1 * A) * (i,j)) * r2 by A7, MATRIX_3:def 6
.= (r1 * (A * (i,j))) * r2 by A6, MATRIX_3:def 5
.= r1 * ((A * (i,j)) * r2) by GROUP_1:def 3
.= r1 * ((A * r2) * (i,j)) by A6, MATRIX_3:def 6
.= (r1 * (A * r2)) * (i,j) by A9, MATRIX_3:def 5 ; :: thesis: verum

end;

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