:: deftheorem Def9 defines with_line_sum=1 MATRPROB:def 9 :
for M being Matrix of REAL holds
( M is with_line_sum=1 iff for k being Nat st k in dom M holds
Sum (M . k) = 1 );