theorem Th28: :: MEASURE9:30

for M being Matrix of ExtREAL st ( for i being Nat st i in dom M holds
not -infty in rng (M . i) ) holds
SumAll M = SumAll (M @)