reconsider n1 = n as Element of NAT by ORDINAL1:def 13;
deffunc H₁( set , set ) -> Element of NAT = 0 ;
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();
A2: for i, j being Element of NAT st [i,j] in Indices M & M * i,j <> 0 holds
i = j by A1;
reconsider M1 = M as Matrix of n, REAL ;
take M1 ; :: thesis: M1 is diagonal
thus M1 is diagonal by A2, Def3; :: thesis: verum