let X be non empty set ; :: thesis: 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.||
let x be Element of X; :: thesis: 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.||
let f be Function of X,COMPLEX; :: thesis: for F being Point of (C_Normed_Algebra_of_BoundedFunctions X) st f = F & f | X is bounded holds
|.(f . x).| <= ||.F.||
let F be Point of (C_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.||
reconsider r = |.(f . x).| as ExtReal ;
A3: r in PreNorms f ;
( not PreNorms f is empty & PreNorms f is bounded_above ) by Th11, A2;
then r <= upper_bound (PreNorms f) by A3, SEQ_4:def 1;
hence |.(f . x).| <= ||.F.|| by A1, A2, Th13; :: thesis: verum