deffunc H₁( set , set ) -> Element of NAT = 0 ;
reconsider n1 = n as Element of NAT by ORDINAL1:def 12;
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