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)