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 A1: 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 A2: ( 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
A3: ( 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:45; :: 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:7;
A4: 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
A5: for n being Element of NAT st n >= k holds
||.((seq . n) - (lim seq)).|| < p by A2, NORMSP_1:def 7;
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 A6: ( n >= k & x in the carrier of X ) ; :: thesis: abs (((H . n) . x) - (f . x)) < p
then A7: ||.((seq . n) - (lim seq)).|| < p by A5;
(seq . n) - (lim seq) in BoundedFunctions the carrier of X ;
then consider g being RealMap of X such that
A8: ( 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
A9: ( s = seq . n & s | the carrier of X is bounded ) ;
reconsider x0 = x as Element of the carrier of X by A6;
A10: g . x0 = (s . x0) - (f . x0) by A8, A9, A3, C0SP1:34;
abs (g . x0) <= ||.((seq . n) - (lim seq)).|| by A8, C0SP1:26;
hence abs (((H . n) . x) - (f . x)) < p by A10, A9, A7, XXREAL_0:2; :: thesis: verum

end;

end;

f is continuous

proof

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
A11: ( 0 < r0 & ].((f . x) - r0),((f . x) + r0).[ c= V ) by RCOMP_1:19;
consider k being Element of NAT such that
A12: 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 A4, A11, XREAL_1:222;
A13: abs (((H . k) . x) - (f . x)) < r0 / 3 by A12;
k in NAT ;
then k in dom seq by NORMSP_1:12;
then H . k in rng seq by FUNCT_1:def 3;
then H . k in Y by A2;
then consider h being continuous RealMap of X such that
A14: H . k = h by A1;
set r1 = h . x;
set G1 = ].((h . x) - (r0 / 3)),((h . x) + (r0 / 3)).[;
A15: h . x < (h . x) + (r0 / 3) by A11, XREAL_1:29, XREAL_1:222;
then (h . x) - (r0 / 3) < h . x by XREAL_1:19;
then h . x in ].((h . x) - (r0 / 3)),((h . x) + (r0 / 3)).[ by A15;
then consider W1 being Subset of X such that
A16: ( x in W1 & W1 is open & h .: W1 c= ].((h . x) - (r0 / 3)),((h . x) + (r0 / 3)).[ ) by Th1;

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
A17: ( z0 in dom f & z0 in W1 & f . z0 = x0 ) by FUNCT_1:def 6;
h . z0 in h .: W1 by A17, FUNCT_2:35;
then ( (h . x) - (r0 / 3) < h . z0 & h . z0 < (h . x) + (r0 / 3) ) by A16, 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:9;
then A18: abs ((h . z0) - (h . x)) <= r0 / 3 by ABSVALUE:5;
A19: abs (- ((h . x) - (f . x))) < r0 / 3 by A13, A14, COMPLEX1:52;
abs ((h . z0) - (f . z0)) < r0 / 3 by A17, A12, A14;
then abs (- ((h . z0) - (f . z0))) < r0 / 3 by COMPLEX1:52;
then (abs ((f . z0) - (h . z0))) + (abs ((f . x) - (h . x))) < (r0 / 3) + (r0 / 3) by A19, XREAL_1:8;
then A20: ((abs ((f . z0) - (h . z0))) + (abs ((f . x) - (h . x)))) + (abs ((h . z0) - (h . x))) < ((r0 / 3) + (r0 / 3)) + (r0 / 3) by A18, XREAL_1:8;
abs ((f . z0) - (f . x)) = abs ((((f . z0) - (h . z0)) - ((f . x) - (h . x))) + ((h . z0) - (h . x))) ;
then A21: abs ((f . z0) - (f . x)) <= (abs (((f . z0) - (h . z0)) - ((f . x) - (h . x)))) + (abs ((h . z0) - (h . x))) by COMPLEX1:56;
abs (((f . z0) - (h . z0)) - ((f . x) - (h . x))) <= (abs ((f . z0) - (h . z0))) + (abs ((f . x) - (h . x))) by COMPLEX1:57;
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:6;
then abs ((f . z0) - (f . x)) <= ((abs ((f . z0) - (h . z0))) + (abs ((f . x) - (h . x)))) + (abs ((h . z0) - (h . x))) by A21, XXREAL_0:2;
then abs ((f . z0) - (f . x)) < r0 by A20, XXREAL_0:2;
then ( - r0 < (f . z0) - (f . x) & (f . z0) - (f . x) < r0 ) by SEQ_2:1;
then ( (- r0) + (f . x) < ((f . z0) - (f . x)) + (f . x) & ((f . z0) - (f . x)) + (f . x) < r0 + (f . x) ) by XREAL_1:6;
hence x0 in ].((f . x) - r0),((f . x) + r0).[ by A17; :: 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 A16, A11, XBOOLE_1:1; :: thesis: verum

end;

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

end;

hence lim seq in Y by A3, A1; :: thesis: verum

end;

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