take M = 1. K,n; :: thesis: M is diagonal
let i be Nat; :: according to MATRIX_1:def 15 :: thesis: for j being Nat st [i,j] in Indices M & M * i,j <> 0. K holds
i = j
let j be Nat; :: thesis: ( [i,j] in Indices M & M * i,j <> 0. K implies i = j )
thus ( [i,j] in Indices M & M * i,j <> 0. K implies i = j ) by Def12; :: thesis: verum