let M be Matrix of REAL; :: thesis: ( M = {} implies SumAll M = 0 )
assume M = {} ; :: thesis: SumAll M = 0
then reconsider M1 = M as Matrix of 0 , width M,REAL by MATRIX_0:13;
len M1 = 0 by MATRIX_0:22;
hence SumAll M = 0 by MATRPROB:23; :: thesis: verum