let M be Matrix of ExtREAL; :: thesis: ( len M = 0 implies SumAll M = 0 )
assume len M = 0 ; :: thesis: SumAll M = 0
then len (Sum M) = 0 by Def5;
then Sum M is empty ;
hence SumAll M = 0 by EXTREAL1:7; :: thesis: verum