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
abs (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
abs (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
abs (f . x) <= ||.F.||
let F be Point of (R_Normed_Algebra_of_BoundedFunctions X); :: thesis: ( f = F & f | X is bounded implies abs (f . x) <= ||.F.|| )
assume A1: ( f = F & f | X is bounded ) ; :: thesis: abs (f . x) <= ||.F.||
then A2: ( not PreNorms f is empty & PreNorms f is bounded_above ) by ThB13;
abs (f . x) in PreNorms f ;
then abs (f . x) <= sup (PreNorms f) by A2, SEQ_4:def 4;
hence abs (f . x) <= ||.F.|| by A1, ThB17; :: thesis: verum