theorem Th58: :: MATRPROB:58

for n, m being non zero Nat ex M being Matrix of n,m,REAL st
( M is m-nonnegative & M is with_line_sum=1 )