let n be Nat; :: thesis: for R being Ring holds (1. (R,n)) @ = 1. (R,n)
let R be Ring; :: thesis: (1. (R,n)) @ = 1. (R,n)

per cases ( n > 0 or n = 0 ) by NAT_1:3;

suppose A1: n > 0 ; :: thesis: (1. (R,n)) @ = 1. (R,n)

A2: len (1. (R,n)) = n by MATRIX_0:24;
A3: Indices (1. (R,n)) = [:(Seg n),(Seg n):] by MATRIX_0:24;
A4: for i, j being Nat st [i,j] in Indices (1. (R,n)) holds
(1. (R,n)) * (i,j) = ((1. (R,n)) @) * (i,j)

proof

let i, j be Nat; :: thesis: ( [i,j] in Indices (1. (R,n)) implies (1. (R,n)) * (i,j) = ((1. (R,n)) @) * (i,j) )
assume A5: [i,j] in Indices (1. (R,n)) ; :: thesis: (1. (R,n)) * (i,j) = ((1. (R,n)) @) * (i,j)
then ( i in Seg n & j in Seg n ) by A3, ZFMISC_1:87;
then A6: [j,i] in Indices (1. (R,n)) by A3, ZFMISC_1:87;

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

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

hence (1. (R,n)) * (i,j) = ((1. (R,n)) @) * (i,j) by A5, MATRIX_0:def 6; :: thesis: verum

end;

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

then ( (1. (R,n)) * (i,j) = 0. R & (1. (R,n)) * (j,i) = 0. R ) by A5, A6, MATRIX_1:def 3;
hence (1. (R,n)) * (i,j) = ((1. (R,n)) @) * (i,j) by A6, MATRIX_0:def 6; :: thesis: verum

end;

end;

end;

A7: width (1. (R,n)) = n by MATRIX_0:24;
then ( len ((1. (R,n)) @) = width (1. (R,n)) & width ((1. (R,n)) @) = len (1. (R,n)) ) by A1, MATRIX_0:54;
hence (1. (R,n)) @ = 1. (R,n) by A7, A2, A4, MATRIX_0:21; :: thesis: verum

end;

suppose n = 0 ; :: thesis: (1. (R,n)) @ = 1. (R,n)

hence (1. (R,n)) @ = 1. (R,n) by MATRIX_0:45; :: thesis: verum

end;

end;