theorem Th18: :: MEASURE9:20

for F, G, H being FinSequence of ExtREAL st not -infty in rng F & not -infty in rng G & dom F = dom G & H = F + G holds
Sum H = (Sum F) + (Sum G)