set E = the diagonal Matrix of 1,K;
take the diagonal Matrix of 1,K ; :: thesis: the diagonal Matrix of 1,K is diagonal
thus the diagonal Matrix of 1,K is diagonal ; :: thesis: verum