:: deftheorem defines SumAll MEASURE9:def 6 :
for M being Matrix of ExtREAL holds SumAll M = Sum (Sum M);