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 V99() & H is V99() holds
SUM F <= (SUM G) + (SUM H)