theorem Th11: :: MEASURE7:11

for F, G being sequence of ExtREAL st G is nonnegative holds
for S being non empty Subset of NAT
for H being Function of S,NAT st H is one-to-one & ( for k being Element of NAT holds
( ( k in S implies F . k = (G * H) . k ) & ( not k in S implies F . k = 0. ) ) ) holds
SUM F <= SUM G