let A be non empty closed_interval Subset of REAL; :: thesis: for v being Point of (R_Normed_Algebra_of_ContinuousFunctions (ClstoCmp A)) holds v in BoundedFunctions the carrier of (ClstoCmp A)
let v be Point of (R_Normed_Algebra_of_ContinuousFunctions (ClstoCmp A)); :: thesis: v in BoundedFunctions the carrier of (ClstoCmp A)
set AV = the carrier of (ClstoCmp A);
R_Algebra_of_ContinuousFunctions (ClstoCmp A) is Subalgebra of R_Algebra_of_BoundedFunctions the carrier of (ClstoCmp A) by C0SP2:9;
then A1: the carrier of (R_Algebra_of_ContinuousFunctions (ClstoCmp A)) c= the carrier of (R_Algebra_of_BoundedFunctions the carrier of (ClstoCmp A)) by C0SP1:def 9;
v in the carrier of (R_Algebra_of_ContinuousFunctions (ClstoCmp A)) ;
hence v in BoundedFunctions the carrier of (ClstoCmp A) by A1; :: thesis: verum