let n be Nat; :: thesis: for MR being Matrix of n, REAL holds
( MR is diagonal iff for i being Element of 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 Element of NAT st i in dom MR holds
Line MR,i has_onlyone_value_in i )
A1: width MR = n by MATRIX_1:25;
len MR = n by MATRIX_1:25;
then A2: dom MR = Seg (width MR) by A1, FINSEQ_1:def 3;

hereby :: thesis: ( ( for i being Element of 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 Element of NAT st i in dom MR holds
Line MR,i has_onlyone_value_in i

now

let i be Element of 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_1:def 8;

A6: now

let j be Element of 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_2:18;
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_1:def 8
.= 0 by A3, A8, A9, Def3 ;
:: 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, Def2; :: thesis: verum

end;

hence for i being Element of NAT st i in dom MR holds
Line MR,i has_onlyone_value_in i ; :: thesis: verum

end;

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

proof

let i, j be Element of 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_2:18;
assume A16: i <> j ; :: thesis: contradiction
len (Line MR,i) = width MR by MATRIX_1:def 8;
then dom (Line MR,i) = Seg (width MR) by FINSEQ_1:def 3;
then MR * i,j = (Line MR,i) . j by A15, MATRIX_1:def 8
.= 0 by A16, A15, A14, Def2 ;
hence contradiction by A12; :: thesis: verum

end;

hence MR is diagonal by Def3; :: thesis: verum