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 that
A1: f = F and
A2: f | X is bounded ; :: thesis: abs (f . x) <= ||.F.||
A3: abs (f . x) in PreNorms f ;
( not PreNorms f is empty & PreNorms f is bounded_above ) by A2, Th17;
then abs (f . x) <= upper_bound (PreNorms f) by A3, SEQ_4:def 1;
hence abs (f . x) <= ||.F.|| by A1, A2, Th21; :: thesis: verum