take
1. (K,n)
; :: thesis: 1. (K,n) is diagonal

let i be Nat; :: according to MATRIX_1:def 6 :: thesis: for j being Nat st [i,j] in Indices (1. (K,n)) & (1. (K,n)) * (i,j) <> 0. K holds

i = j

let j be Nat; :: thesis: ( [i,j] in Indices (1. (K,n)) & (1. (K,n)) * (i,j) <> 0. K implies i = j )

thus ( [i,j] in Indices (1. (K,n)) & (1. (K,n)) * (i,j) <> 0. K implies i = j ) by Def3; :: thesis: verum

let i be Nat; :: according to MATRIX_1:def 6 :: thesis: for j being Nat st [i,j] in Indices (1. (K,n)) & (1. (K,n)) * (i,j) <> 0. K holds

i = j

let j be Nat; :: thesis: ( [i,j] in Indices (1. (K,n)) & (1. (K,n)) * (i,j) <> 0. K implies i = j )

thus ( [i,j] in Indices (1. (K,n)) & (1. (K,n)) * (i,j) <> 0. K implies i = j ) by Def3; :: thesis: verum