let M be Matrix of REAL; :: thesis: ( len M = 0 implies SumAll M = 0 )
assume len M = 0 ; :: thesis: SumAll M = 0
then len (Sum M) = 0 by Def1;
then Sum M = <*> REAL ;
hence SumAll M = 0 by RVSUM_1:72; :: thesis: verum