let R be Ring; :: thesis: for n being Nat
for S being Subring of R holds 1. (S,n) = 1. (R,n)
let n be Nat; :: thesis: for S being Subring of R holds 1. (S,n) = 1. (R,n)
let S be Subring of R; :: thesis: 1. (S,n) = 1. (R,n)
reconsider RHS = 1. (S,n) as Matrix of n,R by Th82;
for i, j being Nat st [i,j] in Indices (1. (R,n)) holds
(1. (R,n)) * (i,j) = RHS * (i,j)

proof

let i, j be Nat; :: thesis: ( [i,j] in Indices (1. (R,n)) implies (1. (R,n)) * (i,j) = RHS * (i,j) )
assume A1: [i,j] in Indices (1. (R,n)) ; :: thesis: (1. (R,n)) * (i,j) = RHS * (i,j)
then A2: [i,j] in Indices RHS by MATRIX_0:26;

per cases ( i = j or i <> j ) ;

suppose A3: i = j ; :: thesis: (1. (R,n)) * (i,j) = RHS * (i,j)

hence (1. (R,n)) * (i,j) = 1. R by A1, MATRIX_1:def 3
.= 1. S by C0SP1:def 3
.= (1. (S,n)) * (i,j) by A2, A3, MATRIX_1:def 3
.= RHS * (i,j) by A2, Th83 ;
:: thesis: verum

end;

suppose A4: i <> j ; :: thesis: (1. (R,n)) * (i,j) = RHS * (i,j)

hence (1. (R,n)) * (i,j) = 0. R by A1, MATRIX_1:def 3
.= 0. S by C0SP1:def 3
.= (1. (S,n)) * (i,j) by A2, A4, MATRIX_1:def 3
.= RHS * (i,j) by A2, Th83 ;
:: thesis: verum

end;

end;

end;

hence 1. (R,n) = 1. (S,n) by MATRIX_0:27; :: thesis: verum