:: deftheorem defines SumAll MATRIXC1:def 11 :
for M being Matrix of COMPLEX holds SumAll M = Sum (LineSum M);