theorem Th24: :: MEASURE9:26

for M1, M2 being Matrix of ExtREAL st ( 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
(Sum M1) + (Sum M2) = Sum (M1 ^^ M2)