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

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