deffunc H1( set , set ) -> Element of REAL = In (0,REAL);
reconsider n1 = n as Nat ;
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) = H1(i,j)
from MATRIX_0:sch 1();
reconsider M1 = M as Matrix of n,REAL ;
take
M1
; M1 is diagonal
for i, j being Nat st [i,j] in Indices M & M * (i,j) <> 0 holds
i = j
by A1;
hence
M1 is diagonal
; verum