let X be non empty set ; :: thesis: 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.||
let x be Element of X; :: thesis: 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.||
let f be Function of X,REAL; :: thesis: for F being Point of (R_Normed_Algebra_of_BoundedFunctions X) st f = F & f | X is bounded holds
|.(f . x).| <= ||.F.||
let F be Point of (R_Normed_Algebra_of_BoundedFunctions X); :: thesis: ( f = F & f | X is bounded implies |.(f . x).| <= ||.F.|| )
assume that
A1: f = F and
A2: f | X is bounded ; :: thesis: |.(f . x).| <= ||.F.||
A3: |.(f . x).| in PreNorms f ;
( not PreNorms f is empty & PreNorms f is bounded_above ) by A2, Th17;
then |.(f . x).| <= upper_bound (PreNorms f) by A3, SEQ_4:def 1;
hence |.(f . x).| <= ||.F.|| by A1, A2, Th20; :: thesis: verum