theorem Th26: :: C0SP1:26

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