theorem Th10: :: MEASURE7:10

for 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 holds
SUM (On (G * H)) <= SUM G