hereby :: thesis: ( ( for i, j being Element of 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 Element of NAT st i in Seg n & j in Seg n & i <> j holds
M * i,j = 0. Klet i,
j be
Element of
NAT ;
:: thesis: ( i in Seg n & j in Seg n & i <> j implies M * i,j = 0. K )assume A2:
(
i in Seg n &
j in Seg n &
i <> j )
;
:: thesis: M * i,j = 0. Kthen
[i,j] in [:(Seg n),(Seg n):]
by ZFMISC_1:def 2;
then
[i,j] in Indices M
by MATRIX_1:25;
hence
M * i,
j = 0. K
by A1, A2, MATRIX_1:def 15;
:: thesis: verum
end;
assume A3:
for i, j being Element of 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 15 :: thesis: ( not [i,j] in Indices M or M * i,j = 0. K or i = j )
assume A4:
( [i,j] in Indices M & M * i,j <> 0. K )
; :: thesis: i = j
then
[i,j] in [:(Seg n),(Seg n):]
by MATRIX_1:25;
then
( i in Seg n & j in Seg n )
by ZFMISC_1:106;
hence
i = j
by A3, A4; :: thesis: verum