let R be Ring; :: thesis: for r, s being Element of R holds
( r * <*<*s*>*> = <*<*(r * s)*>*> & <*<*s*>*> * r = <*<*(s * r)*>*> )
let r, s be Element of R; :: thesis: ( r * <*<*s*>*> = <*<*(r * s)*>*> & <*<*s*>*> * r = <*<*(s * r)*>*> )
set M = <*<*s*>*>;
set M1 = <*<*(r * s)*>*>;
set M2 = <*<*(s * r)*>*>;
for i, j being Nat st [i,j] in Indices (r * <*<*s*>*>) holds
(r * <*<*s*>*>) * (i,j) = <*<*(r * s)*>*> * (i,j)

proof

let i, j be Nat; :: thesis: ( [i,j] in Indices (r * <*<*s*>*>) implies (r * <*<*s*>*>) * (i,j) = <*<*(r * s)*>*> * (i,j) )
assume A1: [i,j] in Indices (r * <*<*s*>*>) ; :: thesis: (r * <*<*s*>*>) * (i,j) = <*<*(r * s)*>*> * (i,j)
A2: Indices (r * <*<*s*>*>) = [:(Seg 1),(Seg 1):] by MATRIX_0:24
.= Indices <*<*s*>*> by MATRIX_0:24 ;
A3: ( i = 1 & j = 1 )

proof

[i,j] in [:(Seg 1),(Seg 1):] by A1, MATRIX_0:24;
then ( i in {1} & j in {1} ) by FINSEQ_1:2, ZFMISC_1:87;
hence ( i = 1 & j = 1 ) by TARSKI:def 1; :: thesis: verum

end;

hence (r * <*<*s*>*>) * (i,j) = r * (<*<*s*>*> * (1,1)) by A1, A2, MATRIX_3:def 5
.= r * s by MATRIX_0:49
.= <*<*(r * s)*>*> * (i,j) by A3, MATRIX_0:49 ;
:: thesis: verum

end;

hence r * <*<*s*>*> = <*<*(r * s)*>*> by MATRIX_0:27; :: thesis: <*<*s*>*> * r = <*<*(s * r)*>*>
for i, j being Nat st [i,j] in Indices (<*<*s*>*> * r) holds
(<*<*s*>*> * r) * (i,j) = <*<*(s * r)*>*> * (i,j)

proof

let i, j be Nat; :: thesis: ( [i,j] in Indices (<*<*s*>*> * r) implies (<*<*s*>*> * r) * (i,j) = <*<*(s * r)*>*> * (i,j) )
assume A4: [i,j] in Indices (<*<*s*>*> * r) ; :: thesis: (<*<*s*>*> * r) * (i,j) = <*<*(s * r)*>*> * (i,j)
A5: Indices (<*<*s*>*> * r) = [:(Seg 1),(Seg 1):] by MATRIX_0:24
.= Indices <*<*s*>*> by MATRIX_0:24 ;
A6: ( i = 1 & j = 1 )

proof

[i,j] in [:(Seg 1),(Seg 1):] by A4, MATRIX_0:24;
then ( i in Seg 1 & j in Seg 1 ) by ZFMISC_1:87;
hence ( i = 1 & j = 1 ) by FINSEQ_1:2, TARSKI:def 1; :: thesis: verum

end;

thus (<*<*s*>*> * r) * (i,j) = (<*<*s*>*> * (i,j)) * r by A4, A5, MATRIX_3:def 6
.= s * r by A6, MATRIX_0:49
.= <*<*(s * r)*>*> * (i,j) by A6, MATRIX_0:49 ; :: thesis: verum

end;

hence <*<*s*>*> * r = <*<*(s * r)*>*> by MATRIX_0:27; :: thesis: verum