:: deftheorem Def7 defines with_sum=1 MATRPROB:def 7 :
for M being Matrix of REAL holds
( M is with_sum=1 iff SumAll M = 1 );