for n being Nat
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 )