let M be Matrix of REAL; :: thesis: ( M is with_sum=1 implies not M is empty-yielding )
assume A1: M is with_sum=1 ; :: thesis: M is empty-yielding
assume A2: M is empty-yielding ; :: thesis: contradiction

per cases ( len M = 0 or ( width M = 0 & len M > 0 ) ) by A2, MATRIX_0:def 10;

suppose len M = 0 ; :: thesis: contradiction

then SumAll M = 0 by MATRPROB:23;
hence contradiction by A1, MATRPROB:def 7; :: thesis: verum

end;

suppose ( width M = 0 & len M > 0 ) ; :: thesis: contradiction

then reconsider M1 = M as Matrix of len M, 0 ,REAL by MATRIX_0:20;
SumAll M1 = 0 by MATRPROB:24;
hence contradiction by A1, MATRPROB:def 7; :: thesis: verum

end;

end;