for n being Nat holds
( ( for i being Nat st [i,i] in Indices (1_Rmatrix n) holds
(1_Rmatrix n) * (i,i) = 1 ) & ( for i, j being Nat st [i,j] in Indices (1_Rmatrix n) & i <> j holds
(1_Rmatrix n) * (i,j) = 0 ) )