hereby ( ( 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
;
for i, j being Nat st i in Seg n & j in Seg n & i <> j holds
M * (i,j) = 0. Klet i,
j be
Nat;
( 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
;
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;
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
; M is diagonal
let i, j be Nat; MATRIX_1:def 6 ( 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
; 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; verum