deffunc H₁( set , set ) -> Element of NAT = 0 ;
reconsider n1 = n as Element of NAT by ORDINAL1:def 13;
consider M being Matrix of n1, REAL such that
A1: for i, j being Nat st [i,j] in Indices M holds
M * i,j = H₁(i,j) from MATRIX_1:sch 1();
reconsider M1 = M as Matrix of n, REAL ;
take M1 ; :: thesis: M1 is diagonal
for i, j being Element of NAT st [i,j] in Indices M & M * i,j <> 0 holds
i = j by A1;
hence M1 is diagonal by Def3; :: thesis: verum