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: not 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, GOBOARD1:def 5;

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_1:20;
SumAll M1 = 0 by MATRPROB:24;
hence contradiction by A1, MATRPROB:def 7; :: thesis: verum

end;

end;