theorem Th25: :: MEASURE9:27

for M1, M2 being Matrix of ExtREAL st len M1 = len M2 & ( for i being Nat st i in dom M1 holds
not -infty in rng (M1 . i) ) & ( for i being Nat st i in dom M2 holds
not -infty in rng (M2 . i) ) holds
(SumAll M1) + (SumAll M2) = SumAll (M1 ^^ M2)