theorem Th1: :: MESFUNC4:1

for F, G, H being FinSequence of ExtREAL st F is nonnegative & G is nonnegative & dom F = dom G & H = F + G holds
Sum H = (Sum F) + (Sum G)