theorem Th10: :: HILB10_5:11

for n being Ordinal
for p being Polynomial of n,F_Real
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 (p,x)).| <= (sum_of_coefficients |.p.|) * (r |^ (degree p))