hereby :: thesis: ( ( for i, j being Nat st i in Seg n & j in Seg n & i <> j holds
M * (i,j) = 0. K ) implies M is diagonal )

assume A1: M is diagonal ; :: thesis: for i, j being Nat st i in Seg n & j in Seg n & i <> j holds
M * (i,j) = 0. K
let i, j be Nat; :: thesis: ( i in Seg n & j in Seg n & i <> j implies M * (i,j) = 0. K )
assume that
A2: ( i in Seg n & j in Seg n ) and
A3: i <> j ; :: thesis: M * (i,j) = 0. K
[i,j] in [:(Seg n),(Seg n):] by A2, ZFMISC_1:def 2;
then [i,j] in Indices M by MATRIX_0:24;
hence M * (i,j) = 0. K by A1, A3; :: thesis: verum

end;

assume A4: for i, j being Nat st i in Seg n & j in Seg n & i <> j holds
M * (i,j) = 0. K ; :: thesis: M is diagonal
let i, j be Nat; :: according to MATRIX_1:def 6 :: thesis: ( not [i,j] in Indices M or M * (i,j) = 0. K or i = j )
assume that
A5: [i,j] in Indices M and
A6: M * (i,j) <> 0. K ; :: thesis: i = j
[i,j] in [:(Seg n),(Seg n):] by A5, MATRIX_0:24;
then ( i in Seg n & j in Seg n ) by ZFMISC_1:87;
hence i = j by A4, A6; :: thesis: verum