let n be Nat; :: thesis: (1_Rmatrix n) @ = 1_Rmatrix n

per cases ( n > 0 or n = 0 ) ;

suppose A1: n > 0 ; :: thesis: (1_Rmatrix n) @ = 1_Rmatrix n

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

proof

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

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

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

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

end;

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

then ( (1_Rmatrix n) * (i0,j0) = 0 & (1_Rmatrix n) * (j0,i0) = 0 ) by A5, A6, Th63;
hence (1_Rmatrix n) * (i,j) = ((1_Rmatrix n) @) * (i,j) by A6, MATRIX_0:def 6; :: thesis: verum

end;

end;

end;

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

end;

suppose n = 0 ; :: thesis: (1_Rmatrix n) @ = 1_Rmatrix n

hence (1_Rmatrix n) @ = 1_Rmatrix n by MATRIX_0:45; :: thesis: verum

end;

end;