let S be non empty compact TopSpace; :: thesis: for T being NormedLinearTopSpace
for Y being Subset of the carrier of (R_NormSpace_of_BoundedFunctions ( the carrier of S,T)) st Y = ContinuousFunctions (S,T) holds
Y is closed
let T be NormedLinearTopSpace; :: thesis: for Y being Subset of the carrier of (R_NormSpace_of_BoundedFunctions ( the carrier of S,T)) st Y = ContinuousFunctions (S,T) holds
Y is closed
let Y be Subset of the carrier of (R_NormSpace_of_BoundedFunctions ( the carrier of S,T)); :: thesis: ( Y = ContinuousFunctions (S,T) implies Y is closed )
assume A1: Y = ContinuousFunctions (S,T) ; :: thesis: Y is closed

now :: thesis: for seq being sequence of (R_NormSpace_of_BoundedFunctions ( the carrier of S,T)) st rng seq c= Y & seq is convergent holds
lim seq in Y

let seq be sequence of (R_NormSpace_of_BoundedFunctions ( the carrier of S,T)); :: 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
reconsider f = lim seq as bounded Function of the carrier of S, the carrier of T by RSSPACE4:def 5;
A3: dom f = the carrier of S by FUNCT_2:def 1;

now :: thesis: for z being object st z in BoundedFunctions ( the carrier of S,T) holds
z in PFuncs ( the carrier of S, the carrier of T)

let z be object ; :: thesis: ( z in BoundedFunctions ( the carrier of S,T) implies z in PFuncs ( the carrier of S, the carrier of T) )
assume z in BoundedFunctions ( the carrier of S,T) ; :: thesis: z in PFuncs ( the carrier of S, the carrier of T)
then z is Function of the carrier of S, the carrier of T by RSSPACE4:def 5;
hence z in PFuncs ( the carrier of S, the carrier of T) by PARTFUN1:45; :: thesis: verum

end;

then BoundedFunctions ( the carrier of S,T) c= PFuncs ( the carrier of S, the carrier of T) ;
then reconsider H = seq as Functional_Sequence of the carrier of S, the carrier of T by FUNCT_2:7;
A4: for n being Nat holds the carrier of S c= dom (H . n)

proof

let n be Nat; :: thesis: the carrier of S c= dom (H . n)
H . n in rng seq by ORDINAL1:def 12, FUNCT_2:4;
then H . n in Y by A2;
then consider f being Function of the carrier of S, the carrier of T such that
A5: ( H . n = f & f is continuous ) by A1;
thus the carrier of S c= dom (H . n) by A5, FUNCT_2:def 1; :: thesis: verum

end;

A6: for p being Real st p > 0 holds
ex k being Nat st
for n being Nat
for x being Element of the carrier of S st n >= k & x in the carrier of S 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 Element of the carrier of S st n >= k & x in the carrier of S holds
||.(((H . n) /. x) - (f /. x)).|| < p )
assume p > 0 ; :: thesis: ex k being Nat st
for n being Nat
for x being Element of the carrier of S st n >= k & x in the carrier of S holds
||.(((H . n) /. x) - (f /. x)).|| < p
then consider k being Nat such that
A7: for n being Nat st n >= k holds
||.((seq . n) - (lim seq)).|| < p by A2, NORMSP_1:def 7;
reconsider k = k as Element of NAT by ORDINAL1:def 12;
take k ; :: thesis: for n being Nat
for x being Element of the carrier of S st n >= k & x in the carrier of S holds
||.(((H . n) /. x) - (f /. x)).|| < p

hereby :: thesis: verum

let n be Nat; :: thesis: for x being Element of S st n >= k & x in the carrier of S holds
||.(((H . n) /. x) - (f /. x)).|| < p
let x be Element of S; :: thesis: ( n >= k & x in the carrier of S implies ||.(((H . n) /. x) - (f /. x)).|| < p )
assume ( n >= k & x in the carrier of S ) ; :: thesis: ||.(((H . n) /. x) - (f /. x)).|| < p
then A8: ||.((seq . n) - (lim seq)).|| < p by A7;
reconsider g = (seq . n) - (lim seq) as bounded Function of the carrier of S, the carrier of T by RSSPACE4:def 5;
reconsider s = seq . n as bounded Function of the carrier of S, the carrier of T by RSSPACE4:def 5;
reconsider x0 = x as Element of the carrier of S ;
A9: g . x0 = (s . x0) - (f . x0) by RSSPACE4:24;
A10: ||.(g . x0).|| <= ||.((seq . n) - (lim seq)).|| by RSSPACE4:16;
H . n in rng seq by ORDINAL1:def 12, FUNCT_2:4;
then H . n in Y by A2;
then ex f being Function of the carrier of S, the carrier of T st
( H . n = f & f is continuous ) by A1;
then dom (H . n) = the carrier of S by FUNCT_2:def 1;
then (H . n) . x = (H . n) /. x by PARTFUN1:def 6;
hence ||.(((H . n) /. x) - (f /. x)).|| < p by A9, A10, A8, XXREAL_0:2; :: thesis: verum

end;

end;

A12: for x being Element of the carrier of S st x in the carrier of S holds
for p being Real st p > 0 holds
ex k being Nat st
for n being Nat st n >= k holds
||.(((H . n) /. x) - (f /. x)).|| < p

proof

let x be Element of the carrier of S; :: thesis: ( x in the carrier of S implies for p being Real st p > 0 holds
ex k being Nat st
for n being Nat st n >= k holds
||.(((H . n) /. x) - (f /. x)).|| < p )
assume x in the carrier of S ; :: thesis: for p being Real st p > 0 holds
ex k being Nat st
for n being Nat st n >= k holds
||.(((H . n) /. x) - (f /. x)).|| < p
let p be Real; :: thesis: ( p > 0 implies ex k being Nat st
for n being Nat st n >= k holds
||.(((H . n) /. x) - (f /. x)).|| < p )
assume p > 0 ; :: thesis: ex k being Nat st
for n being Nat st n >= k holds
||.(((H . n) /. x) - (f /. x)).|| < p
then consider k being Nat such that
A13: for n being Nat
for x being Element of the carrier of S st n >= k & x in the carrier of S holds
||.(((H . n) /. x) - (f /. x)).|| < p by A6;
take k ; :: thesis: for n being Nat st n >= k holds
||.(((H . n) /. x) - (f /. x)).|| < p
let n be Nat; :: thesis: ( n >= k implies ||.(((H . n) /. x) - (f /. x)).|| < p )
assume n >= k ; :: thesis: ||.(((H . n) /. x) - (f /. x)).|| < p
hence ||.(((H . n) /. x) - (f /. x)).|| < p by A13; :: thesis: verum

end;

then A14: H is_point_conv_on the carrier of S by A4, SEQFUNC:def 9, A3;
A15: H is_unif_conv_on the carrier of S by A3, A4, SEQFUNC:def 9, A6;
A16: lim (H, the carrier of S) = f by A3, A12, A14, SEQFUNC2:11;
for n being Nat ex Hn being Function of S,T st
( Hn = H . n & Hn is continuous )

proof

let n be Nat; :: thesis: ex Hn being Function of S,T st
( Hn = H . n & Hn is continuous )
H . n in rng seq by ORDINAL1:def 12, FUNCT_2:4;
then H . n in Y by A2;
then consider f being Function of the carrier of S, the carrier of T such that
A17: ( H . n = f & f is continuous ) by A1;
thus ex Hn being Function of S,T st
( Hn = H . n & Hn is continuous ) by A17; :: thesis: verum

end;

then f is continuous by Th49, A15, A16;
hence lim seq in Y by A1; :: thesis: verum

end;

hence Y is closed ; :: thesis: verum