let n be Nat; :: thesis: for MR being Matrix of n,REAL holds
( MR is diagonal iff for i being Nat st i in dom MR holds
Line (MR,i) has_onlyone_value_in i )
let MR be Matrix of n,REAL; :: thesis: ( MR is diagonal iff for i being Nat st i in dom MR holds
Line (MR,i) has_onlyone_value_in i )
A1: width MR = n by MATRIX_0:24;
len MR = n by MATRIX_0:24;
then A2: dom MR = Seg (width MR) by A1, FINSEQ_1:def 3;

hereby :: thesis: ( ( for i being Nat st i in dom MR holds
Line (MR,i) has_onlyone_value_in i ) implies MR is diagonal )

assume A3: MR is diagonal ; :: thesis: for i being Nat st i in dom MR holds
Line (MR,i) has_onlyone_value_in i

now :: thesis: for i being Nat st i in dom MR holds
Line (MR,i) has_onlyone_value_in i

let i be Nat; :: thesis: ( i in dom MR implies Line (MR,i) has_onlyone_value_in i )
assume A4: i in dom MR ; :: thesis: Line (MR,i) has_onlyone_value_in i
A5: len (Line (MR,i)) = width MR by MATRIX_0:def 7;

A6: now :: thesis: for j being Nat st j in dom (Line (MR,i)) & j <> i holds
(Line (MR,i)) . j = 0

let j be Nat; :: thesis: ( j in dom (Line (MR,i)) & j <> i implies (Line (MR,i)) . j = 0 )
assume that
A7: j in dom (Line (MR,i)) and
A8: j <> i ; :: thesis: (Line (MR,i)) . j = 0
j in dom (MR . i) by A4, A7, MATRIX_0:60;
then A9: [i,j] in Indices MR by A4, MATRPROB:13;
j in Seg (width MR) by A5, A7, FINSEQ_1:def 3;
hence (Line (MR,i)) . j = MR * (i,j) by MATRIX_0:def 7
.= 0 by A3, A8, A9 ;
:: thesis: verum

end;

i in dom (Line (MR,i)) by A2, A4, A5, FINSEQ_1:def 3;
hence Line (MR,i) has_onlyone_value_in i by A6; :: thesis: verum

end;

hence for i being Nat st i in dom MR holds
Line (MR,i) has_onlyone_value_in i ; :: thesis: verum

end;

assume A10: for i being Nat st i in dom MR holds
Line (MR,i) has_onlyone_value_in i ; :: thesis: MR is diagonal
for i, j being Nat st [i,j] in Indices MR & MR * (i,j) <> 0 holds
i = j

proof

let i, j be Nat; :: thesis: ( [i,j] in Indices MR & MR * (i,j) <> 0 implies i = j )
assume that
A11: [i,j] in Indices MR and
A12: MR * (i,j) <> 0 ; :: thesis: i = j
A13: i in dom MR by A11, MATRPROB:13;
then A14: Line (MR,i) has_onlyone_value_in i by A10;
j in dom (MR . i) by A11, MATRPROB:13;
then A15: j in dom (Line (MR,i)) by A13, MATRIX_0:60;
assume A16: i <> j ; :: thesis: contradiction
len (Line (MR,i)) = width MR by MATRIX_0:def 7;
then dom (Line (MR,i)) = Seg (width MR) by FINSEQ_1:def 3;
then MR * (i,j) = (Line (MR,i)) . j by A15, MATRIX_0:def 7
.= 0 by A16, A15, A14 ;
hence contradiction by A12; :: thesis: verum

end;

hence MR is diagonal ; :: thesis: verum