let X be non empty compact TopSpace; :: thesis: for Y being Subset of (R_Normed_Algebra_of_BoundedFunctions the carrier of X) st Y = ContinuousFunctions X holds
Y is closed
let Y be Subset of (R_Normed_Algebra_of_BoundedFunctions the carrier of X); :: thesis: ( Y = ContinuousFunctions X implies Y is closed )
assume AS0: Y = ContinuousFunctions X ; :: thesis: Y is closed

now

let seq be sequence of (R_Normed_Algebra_of_BoundedFunctions the carrier of X); :: thesis: ( rng seq c= Y & seq is convergent implies lim seq in Y )
assume AS1: ( rng seq c= Y & seq is convergent ) ; :: thesis: lim seq in Y
lim seq in BoundedFunctions the carrier of X ;
then consider f being Function of the carrier of X,REAL such that
AS2: ( f = lim seq & f | the carrier of X is bounded ) ;

now

let z be set ; :: thesis: ( z in BoundedFunctions the carrier of X implies z in PFuncs the carrier of X,REAL )
assume z in BoundedFunctions the carrier of X ; :: thesis: z in PFuncs the carrier of X,REAL
then ex f being RealMap of X st
( f = z & f | the carrier of X is bounded ) ;
hence z in PFuncs the carrier of X,REAL by PARTFUN1:119; :: thesis: verum

end;

then BoundedFunctions the carrier of X c= PFuncs the carrier of X,REAL by TARSKI:def 3;
then reconsider H = seq as Functional_Sequence of the carrier of X,REAL by FUNCT_2:9;
A1: for p being Real st p > 0 holds
ex k being Element of NAT st
for n being Element of NAT
for x being set st n >= k & x in the carrier of X holds
abs (((H . n) . x) - (f . x)) < p

proof

let p be Real; :: thesis: ( p > 0 implies ex k being Element of NAT st
for n being Element of NAT
for x being set st n >= k & x in the carrier of X holds
abs (((H . n) . x) - (f . x)) < p )
assume p > 0 ; :: thesis: ex k being Element of NAT st
for n being Element of NAT
for x being set st n >= k & x in the carrier of X holds
abs (((H . n) . x) - (f . x)) < p
then consider k being Element of NAT such that
A2: for n being Element of NAT st n >= k holds
||.((seq . n) - (lim seq)).|| < p by AS1, NORMSP_1:def 11;
take k ; :: thesis: for n being Element of NAT
for x being set st n >= k & x in the carrier of X holds
abs (((H . n) . x) - (f . x)) < p

hereby :: thesis: verum

let n be Element of NAT ; :: thesis: for x being set st n >= k & x in the carrier of X holds
abs (((H . n) . x) - (f . x)) < p
let x be set ; :: thesis: ( n >= k & x in the carrier of X implies abs (((H . n) . x) - (f . x)) < p )
assume A3: ( n >= k & x in the carrier of X ) ; :: thesis: abs (((H . n) . x) - (f . x)) < p
then A4: ||.((seq . n) - (lim seq)).|| < p by A2;
(seq . n) - (lim seq) in BoundedFunctions the carrier of X ;
then consider g being RealMap of X such that
A5: ( g = (seq . n) - (lim seq) & g | the carrier of X is bounded ) ;
seq . n in BoundedFunctions the carrier of X ;
then consider s being RealMap of X such that
A6: ( s = seq . n & s | the carrier of X is bounded ) ;
reconsider x0 = x as Element of the carrier of X by A3;
A7: g . x0 = (s . x0) - (f . x0) by C0SP1:35, A5, A6, AS2;
abs (g . x0) <= ||.((seq . n) - (lim seq)).|| by A5, C0SP1:27;
hence abs (((H . n) . x) - (f . x)) < p by A7, A6, XXREAL_0:2, A4; :: thesis: verum

end;

end;

f is continuous

proof

consider n being Element of NAT , x, y being set ;
for x being Point of X
for V being Subset of REAL st f . x in V & V is open holds
ex W being Subset of X st
( x in W & W is open & f .: W c= V )

proof

let x be Point of X; :: thesis: for V being Subset of REAL st f . x in V & V is open holds
ex W being Subset of X st
( x in W & W is open & f .: W c= V )
let V be Subset of REAL ; :: thesis: ( f . x in V & V is open implies ex W being Subset of X st
( x in W & W is open & f .: W c= V ) )
set r = f . x;
assume ( f . x in V & V is open ) ; :: thesis: ex W being Subset of X st
( x in W & W is open & f .: W c= V )
then consider r0 being real number such that
A8: ( 0 < r0 & ].((f . x) - r0),((f . x) + r0).[ c= V ) by RCOMP_1:40;
consider k being Element of NAT such that
A9: for n being Element of NAT
for x being set st n >= k & x in the carrier of X holds
abs (((H . n) . x) - (f . x)) < r0 / 3 by A1, A8, XREAL_1:224;
A10: abs (((H . k) . x) - (f . x)) < r0 / 3 by A9;
k in NAT ;
then k in dom seq by NORMSP_1:17;
then H . k in rng seq by FUNCT_1:def 5;
then H . k in Y by AS1;
then consider h being continuous RealMap of X such that
A11: H . k = h by AS0;
set r1 = h . x;
set G1 = ].((h . x) - (r0 / 3)),((h . x) + (r0 / 3)).[;
A12: h . x < (h . x) + (r0 / 3) by A8, XREAL_1:224, XREAL_1:31;
then (h . x) - (r0 / 3) < h . x by XREAL_1:21;
then h . x in ].((h . x) - (r0 / 3)),((h . x) + (r0 / 3)).[ by A12;
then consider W1 being Subset of X such that
A13: ( x in W1 & W1 is open & h .: W1 c= ].((h . x) - (r0 / 3)),((h . x) + (r0 / 3)).[ ) by LMcont;

now

let x0 be set ; :: thesis: ( x0 in f .: W1 implies x0 in ].((f . x) - r0),((f . x) + r0).[ )
assume x0 in f .: W1 ; :: thesis: x0 in ].((f . x) - r0),((f . x) + r0).[
then consider z0 being set such that
A14: ( z0 in dom f & z0 in W1 & f . z0 = x0 ) by FUNCT_1:def 12;
h . z0 in h .: W1 by FUNCT_2:43, A14;
then ( (h . x) - (r0 / 3) < h . z0 & h . z0 < (h . x) + (r0 / 3) ) by A13, XXREAL_1:4;
then ( ((h . x) - (r0 / 3)) - (h . x) < (h . z0) - (h . x) & (h . z0) - (h . x) < ((h . x) + (r0 / 3)) - (h . x) ) by XREAL_1:11;
then A15: abs ((h . z0) - (h . x)) <= r0 / 3 by ABSVALUE:12;
A16: abs (- ((h . x) - (f . x))) < r0 / 3 by A10, A11, COMPLEX1:138;
abs ((h . z0) - (f . z0)) < r0 / 3 by A14, A9, A11;
then abs (- ((h . z0) - (f . z0))) < r0 / 3 by COMPLEX1:138;
then (abs ((f . z0) - (h . z0))) + (abs ((f . x) - (h . x))) < (r0 / 3) + (r0 / 3) by A16, XREAL_1:10;
then A17: ((abs ((f . z0) - (h . z0))) + (abs ((f . x) - (h . x)))) + (abs ((h . z0) - (h . x))) < ((r0 / 3) + (r0 / 3)) + (r0 / 3) by A15, XREAL_1:10;
abs ((f . z0) - (f . x)) = abs ((((f . z0) - (h . z0)) - ((f . x) - (h . x))) + ((h . z0) - (h . x))) ;
then A18: abs ((f . z0) - (f . x)) <= (abs (((f . z0) - (h . z0)) - ((f . x) - (h . x)))) + (abs ((h . z0) - (h . x))) by COMPLEX1:142;
abs (((f . z0) - (h . z0)) - ((f . x) - (h . x))) <= (abs ((f . z0) - (h . z0))) + (abs ((f . x) - (h . x))) by COMPLEX1:143;
then (abs (((f . z0) - (h . z0)) - ((f . x) - (h . x)))) + (abs ((h . z0) - (h . x))) <= ((abs ((f . z0) - (h . z0))) + (abs ((f . x) - (h . x)))) + (abs ((h . z0) - (h . x))) by XREAL_1:8;
then abs ((f . z0) - (f . x)) <= ((abs ((f . z0) - (h . z0))) + (abs ((f . x) - (h . x)))) + (abs ((h . z0) - (h . x))) by A18, XXREAL_0:2;
then abs ((f . z0) - (f . x)) < r0 by A17, XXREAL_0:2;
then ( - r0 < (f . z0) - (f . x) & (f . z0) - (f . x) < r0 ) by SEQ_2:9;
then ( (- r0) + (f . x) < ((f . z0) - (f . x)) + (f . x) & ((f . z0) - (f . x)) + (f . x) < r0 + (f . x) ) by XREAL_1:8;
hence x0 in ].((f . x) - r0),((f . x) + r0).[ by A14; :: thesis: verum

end;

then f .: W1 c= ].((f . x) - r0),((f . x) + r0).[ by TARSKI:def 3;
hence ex W being Subset of X st
( x in W & W is open & f .: W c= V ) by A13, A8, XBOOLE_1:1; :: thesis: verum

end;

hence f is continuous by LMcont; :: thesis: verum

end;

hence lim seq in Y by AS2, AS0; :: thesis: verum

end;

hence Y is closed by NFCONT_1:def 5; :: thesis: verum