:: deftheorem defines SumAll MATRPROB:def 3 :
for M being Matrix of REAL holds SumAll M = Sum (Sum M);