let M be Matrix of REAL; :: thesis: ( M is with_sum=1 implies not M is V3() )
assume A1: M is with_sum=1 ; :: thesis: M is V3()
assume A2: M is V3() ; :: 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;