theorem Th1: :: MEASURE3:1

for F1, F2 being sequence of ExtREAL st ( for n being Element of NAT holds (Ser F1) . n <= (Ser F2) . n ) holds
SUM F1 <= SUM F2