set M = the diagonal Matrix of n,K;
take the diagonal Matrix of n,K ; :: thesis: ( the diagonal Matrix of n,K is lower_triangular & the diagonal Matrix of n,K is upper_triangular )
thus ( the diagonal Matrix of n,K is lower_triangular & the diagonal Matrix of n,K is upper_triangular ) ; :: thesis: verum