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

now :: thesis: for seq being sequence of (C_Normed_Algebra_of_BoundedFunctions the carrier of X) st rng seq c= Y & seq is convergent holds
lim seq in Y

let seq be sequence of (C_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 ComplexBoundedFunctions the carrier of X ;
then consider f being Function of the carrier of X,COMPLEX such that
A3: ( f = lim seq & f | the carrier of X is bounded ) ;

now :: thesis: for z being object st z in ComplexBoundedFunctions the carrier of X holds
z in PFuncs ( the carrier of X,COMPLEX)

let z be object ; :: thesis: ( z in ComplexBoundedFunctions the carrier of X implies z in PFuncs ( the carrier of X,COMPLEX) )
assume z in ComplexBoundedFunctions the carrier of X ; :: thesis: z in PFuncs ( the carrier of X,COMPLEX)
then ex f being Function of the carrier of X,COMPLEX st
( f = z & f | the carrier of X is bounded ) ;
hence z in PFuncs ( the carrier of X,COMPLEX) by PARTFUN1:45; :: thesis: verum

end;

then ComplexBoundedFunctions the carrier of X c= PFuncs ( the carrier of X,COMPLEX) ;
then reconsider H = seq as Functional_Sequence of the carrier of X,COMPLEX by FUNCT_2:7;
A4: for p being Real st p > 0 holds
ex k being Nat st
for n being Nat
for x being set st n >= k & x in the carrier of X holds
|.(((H . n) . x) - (f . x)).| < p

proof

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

hereby :: thesis: verum

let n be Nat; :: thesis: for x being set st n >= k & x in the carrier of X holds
|.(((H . n) . x) - (f . x)).| < p
let x be set ; :: thesis: ( n >= k & x in the carrier of X implies |.(((H . n) . x) - (f . x)).| < p )
assume A6: ( n >= k & x in the carrier of X ) ; :: thesis: |.(((H . n) . x) - (f . x)).| < p
then A7: ||.((seq . n) - (lim seq)).|| < p by A5;
(seq . n) - (lim seq) in ComplexBoundedFunctions the carrier of X ;
then consider g being Function of the carrier of X,COMPLEX such that
A8: ( g = (seq . n) - (lim seq) & g | the carrier of X is bounded ) ;
seq . n in ComplexBoundedFunctions the carrier of X ;
then consider s being Function of the carrier of X,COMPLEX 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, CC0SP1:26;
|.(g . x0).| <= ||.((seq . n) - (lim seq)).|| by A8, CC0SP1:19;
hence |.(((H . n) . x) - (f . x)).| < p by A10, A9, A7, XXREAL_0:2; :: thesis: verum

end;

end;

f is continuous

proof

set n = the Element of NAT ;
for x being Point of X
for V being Subset of COMPLEX 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 COMPLEX 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 COMPLEX; :: 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 ) )
assume A11: ( 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 )
reconsider z0 = f . x as Complex ;
consider N being Neighbourhood of z0 such that
A12: N c= V by A11, CFDIFF_1:9;
consider r being Real such that
A13: ( 0 < r & { p where p is Complex : |.(p - z0).| < r } c= N ) by CFDIFF_1:def 5;
set S = { p where p is Complex : |.(p - z0).| < r } ;
A14: ( r / 3 > 0 & r / 3 is Real ) by A13;
consider k being Nat such that
A15: for n being Nat
for x being set st n >= k & x in the carrier of X holds
|.(((H . n) . x) - (f . x)).| < r / 3 by A4, A14;
k in NAT by ORDINAL1:def 12;
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 Function of the carrier of X,COMPLEX such that
A16: H . k = h by A1;
set z1 = h . x;
set G1 = { p where p is Complex : |.(p - (h . x)).| < r / 3 } ;
{ p where p is Complex : |.(p - (h . x)).| < r / 3 } c= COMPLEX

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in { p where p is Complex : |.(p - (h . x)).| < r / 3 } or z in COMPLEX )
assume z in { p where p is Complex : |.(p - (h . x)).| < r / 3 } ; :: thesis: z in COMPLEX
then ex y being Complex st
( z = y & |.(y - (h . x)).| < r / 3 ) ;
hence z in COMPLEX by XCMPLX_0:def 2; :: thesis: verum

end;

then reconsider T1 = { p where p is Complex : |.(p - (h . x)).| < r / 3 } as Subset of COMPLEX ;
A17: T1 is open by CFDIFF_1:13;
|.((h . x) - (h . x)).| = 0 ;
then h . x in { p where p is Complex : |.(p - (h . x)).| < r / 3 } by A13;
then consider W1 being Subset of X such that
A18: ( x in W1 & W1 is open & h .: W1 c= { p where p is Complex : |.(p - (h . x)).| < r / 3 } ) by A17, Th3;

now :: thesis: for zz0 being object st zz0 in f .: W1 holds
zz0 in { p where p is Complex : |.(p - z0).| < r }

let zz0 be object ; :: thesis: ( zz0 in f .: W1 implies zz0 in { p where p is Complex : |.(p - z0).| < r } )
assume zz0 in f .: W1 ; :: thesis: zz0 in { p where p is Complex : |.(p - z0).| < r }
then consider xx0 being object such that
A19: ( xx0 in dom f & xx0 in W1 & f . xx0 = zz0 ) by FUNCT_1:def 6;
h . xx0 in h .: W1 by A19, FUNCT_2:35;
then h . xx0 in { p where p is Complex : |.(p - (h . x)).| < r / 3 } by A18;
then consider hx0 being Complex such that
A20: ( hx0 = h . xx0 & |.(hx0 - (h . x)).| < r / 3 ) ;
|.((h . xx0) - (f . xx0)).| < r / 3 by A19, A15, A16;
then |.(- ((h . xx0) - (f . xx0))).| < r / 3 by COMPLEX1:52;
then A21: |.((f . xx0) - (h . xx0)).| < r / 3 ;
A22: |.((h . x) - (f . x)).| < r / 3 by A15, A16;
|.((f . xx0) - (h . xx0)).| + |.((h . xx0) - (h . x)).| < (r / 3) + (r / 3) by A20, A21, XREAL_1:8;
then (|.((f . xx0) - (h . xx0)).| + |.((h . xx0) - (h . x)).|) + |.((h . x) - (f . x)).| < ((r / 3) + (r / 3)) + (r / 3) by A22, XREAL_1:8;
then A23: (|.((f . xx0) - (h . xx0)).| + |.((h . xx0) - (h . x)).|) + |.((h . x) - (f . x)).| < r ;
|.((f . xx0) - (f . x)).| = |.((((f . xx0) - (h . xx0)) + ((h . xx0) - (h . x))) + ((h . x) - (f . x))).| ;
then A24: |.((f . xx0) - (f . x)).| <= |.(((f . xx0) - (h . xx0)) + ((h . xx0) - (h . x))).| + |.((h . x) - (f . x)).| by COMPLEX1:56;
|.(((f . xx0) - (h . xx0)) + ((h . xx0) - (h . x))).| <= |.((f . xx0) - (h . xx0)).| + |.((h . xx0) - (h . x)).| by COMPLEX1:56;
then |.(((f . xx0) - (h . xx0)) + ((h . xx0) - (h . x))).| + |.((h . x) - (f . x)).| <= (|.((f . xx0) - (h . xx0)).| + |.((h . xx0) - (h . x)).|) + |.((h . x) - (f . x)).| by XREAL_1:6;
then |.((f . xx0) - (f . x)).| <= (|.((f . xx0) - (h . xx0)).| + |.((h . xx0) - (h . x)).|) + |.((h . x) - (f . x)).| by A24, XXREAL_0:2;
then |.((f . xx0) - (f . x)).| < r by A23, XXREAL_0:2;
hence zz0 in { p where p is Complex : |.(p - z0).| < r } by A19; :: thesis: verum

end;

then f .: W1 c= { p where p is Complex : |.(p - z0).| < r } ;
then f .: W1 c= N by A13;
hence ex W being Subset of X st
( x in W & W is open & f .: W c= V ) by A18, A12, XBOOLE_1:1; :: thesis: verum

end;

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

end;

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

end;

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