theorem Th19: :: CC0SP1:19

for X being non empty set
for x being Element of X
for f being Function of X,COMPLEX
for F being Point of (C_Normed_Algebra_of_BoundedFunctions X) st f = F & f | X is bounded holds
|.(f . x).| <= ||.F.||