for G being sequence of ExtREAL st G is V99() 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