let n be Nat; :: thesis: ( ( 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 ) )
set K = F_Real ;
thus for i being Nat st [i,i] in Indices (1_Rmatrix n) holds
(1_Rmatrix n) * (i,i) = 1 :: thesis: for i, j being Nat st [i,j] in Indices (1_Rmatrix n) & i <> j holds
(1_Rmatrix n) * (i,j) = 0

proof

let i be Nat; :: thesis: ( [i,i] in Indices (1_Rmatrix n) implies (1_Rmatrix n) * (i,i) = 1 )
assume [i,i] in Indices (1_Rmatrix n) ; :: thesis: (1_Rmatrix n) * (i,i) = 1
hence (1_Rmatrix n) * (i,i) = 1_ F_Real by MATRIX_1:def 3
.= 1 ;
:: thesis: verum

end;

let i, j be Nat; :: thesis: ( [i,j] in Indices (1_Rmatrix n) & i <> j implies (1_Rmatrix n) * (i,j) = 0 )
assume ( [i,j] in Indices (1_Rmatrix n) & i <> j ) ; :: thesis: (1_Rmatrix n) * (i,j) = 0
hence (1_Rmatrix n) * (i,j) = 0. F_Real by MATRIX_1:def 3
.= 0 ;
:: thesis: verum