theorem Th3: :: MEASURE7:3

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