let A be non empty closed_interval Subset of REAL; :: thesis: for u being Function holds
( u is Point of (R_Normed_Algebra_of_ContinuousFunctions (ClstoCmp A)) iff ( dom u = A & u is continuous PartFunc of REAL,REAL ) )
let u be Function; :: thesis: ( u is Point of (R_Normed_Algebra_of_ContinuousFunctions (ClstoCmp A)) iff ( dom u = A & u is continuous PartFunc of REAL,REAL ) )
consider a, b being Real such that
A1: ( a <= b & [.a,b.] = A & ClstoCmp A = Closed-Interval-TSpace (a,b) ) by Def7ClstoCmp;

hereby :: thesis: ( dom u = A & u is continuous PartFunc of REAL,REAL implies u is Point of (R_Normed_Algebra_of_ContinuousFunctions (ClstoCmp A)) )

assume u is Point of (R_Normed_Algebra_of_ContinuousFunctions (ClstoCmp A)) ; :: thesis: ( dom u = A & u is continuous PartFunc of REAL,REAL )
then u in ContinuousFunctions (ClstoCmp A) ;
then consider w being continuous RealMap of (ClstoCmp A) such that
A2: u = w ;
B3: dom w = the carrier of (ClstoCmp A) by FUNCT_2:def 1;
then dom w = A by Lm1;
then ( dom w c= REAL & rng w c= REAL ) ;
then reconsider v = w as PartFunc of REAL,REAL by RELSET_1:4;
v is continuous PartFunc of REAL,REAL by A1, Th80b;
hence ( dom u = A & u is continuous PartFunc of REAL,REAL ) by A2, B3, Lm1; :: thesis: verum

end;

assume A4: ( dom u = A & u is continuous PartFunc of REAL,REAL ) ; :: thesis: u is Point of (R_Normed_Algebra_of_ContinuousFunctions (ClstoCmp A))
then A5: dom u = the carrier of (ClstoCmp A) by Lm1;
rng u c= REAL by A4, RELAT_1:def 19;
then reconsider v = u as RealMap of (ClstoCmp A) by A5, FUNCT_2:2;
v is continuous by A1, A4, Th80b;
then v in the carrier of (R_Normed_Algebra_of_ContinuousFunctions (ClstoCmp A)) ;
hence u is Point of (R_Normed_Algebra_of_ContinuousFunctions (ClstoCmp A)) ; :: thesis: verum