deffunc H₁( 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) = H₁(i,j) from MATRIX_0:sch 1();
reconsider M1 = M as Matrix of n,REAL ;
take M1 ; :: thesis: 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 ; :: thesis: verum