:: deftheorem def6 defines diagonal MATRIX_1:def 6 :
for K being non empty ZeroStr
for M being Matrix of K holds
( M is diagonal iff for i, j being Nat st [i,j] in Indices M & M * (i,j) <> 0. K holds
i = j );