let A be non empty closed_interval Subset of REAL; 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; ( 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;
assume A4:
( dom u = A & u is continuous PartFunc of REAL,REAL )
; 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))
; verum