theorem Th4: :: MEASURE7:4

for F, G, H being sequence of ExtREAL st ( for n being Element of NAT holds F . n = (G . n) + (H . n) ) & G is nonnegative & H is nonnegative holds
SUM F <= (SUM G) + (SUM H)