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

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