theorem Th9: :: HILB10_5:10

for n being Ordinal
for b being bag of n
for r being Real st r >= 1 holds
for x being Function of n, the carrier of F_Real st ( for i being object st i in dom x holds
|.(x . i).| <= r ) holds
|.(eval (b,x)).| <= r |^ (degree b)