let X be non empty closed_interval Subset of REAL; :: thesis: for Y being RealNormSpace
for C being Subset of (R_NormSpace_of_BoundedFunctions (X,Y)) st C = ContinuousFunctions (X,Y) holds
C is closed
let Y be RealNormSpace; :: thesis: for C being Subset of (R_NormSpace_of_BoundedFunctions (X,Y)) st C = ContinuousFunctions (X,Y) holds
C is closed
let C be Subset of (R_NormSpace_of_BoundedFunctions (X,Y)); :: thesis: ( C = ContinuousFunctions (X,Y) implies C is closed )
assume A1: C = ContinuousFunctions (X,Y) ; :: thesis: C is closed

now :: thesis: for seq being sequence of (R_NormSpace_of_BoundedFunctions (X,Y)) st rng seq c= C & seq is convergent holds
lim seq in C

let seq be sequence of (R_NormSpace_of_BoundedFunctions (X,Y)); :: thesis: ( rng seq c= C & seq is convergent implies lim seq in C )
assume A2: ( rng seq c= C & seq is convergent ) ; :: thesis: lim seq in C
reconsider f = lim seq as bounded Function of X,Y by RSSPACE4:def 5;
A3: dom f = X by FUNCT_2:def 1;

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

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

end;

then BoundedFunctions (X,Y) c= PFuncs (X, the carrier of Y) by TARSKI:def 3;
then reconsider H = seq as Functional_Sequence of X, the carrier of Y 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 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 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 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, NORMSP_1:def 7;
take k ; :: thesis: for n being Nat
for x being set st n >= k & x in 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 X holds
||.(((H . n) /. x) - (f /. x)).|| < p
let x be set ; :: thesis: ( n >= k & x in X implies ||.(((H . n) /. x) - (f /. x)).|| < p )
assume A6: ( n >= k & x in X ) ; :: thesis: ||.(((H . n) /. x) - (f /. x)).|| < p
then A7: ||.((seq . n) - (lim seq)).|| < p by A5;
reconsider g = (seq . n) - (lim seq), s = seq . n as bounded Function of X,Y by RSSPACE4:def 5;
reconsider x0 = x as Element of X by A6;
A8: g . x0 = (s /. x0) - (f /. x0) by RSSPACE4:24;
||.(g . x0).|| <= ||.((seq . n) - (lim seq)).|| by RSSPACE4:16;
hence ||.(((H . n) /. x) - (f /. x)).|| < p by A8, A7, XXREAL_0:2; :: thesis: verum

end;

end;

dom f = X by FUNCT_2:def 1;
then ( dom f c= REAL & rng f c= the carrier of Y ) ;
then f in PFuncs (REAL, the carrier of Y) by PARTFUN1:def 3;
then reconsider f = f as PartFunc of REAL,Y by PARTFUN1:46;
for x0 being Real st x0 in dom f holds
f is_continuous_in x0

proof

let x be Real; :: thesis: ( x in dom f implies f is_continuous_in x )
assume A9: x in dom f ; :: thesis: f is_continuous_in x

now :: thesis: for r0 being Real st 0 < r0 holds
ex w1 being Real st
( 0 < w1 & ( for z0 being Real st z0 in dom f & |.(z0 - x).| < w1 holds
||.((f /. z0) - (f /. x)).|| < r0 ) )

let r0 be Real; :: thesis: ( 0 < r0 implies ex w1 being Real st
( 0 < w1 & ( for z0 being Real st z0 in dom f & |.(z0 - x).| < w1 holds
||.((f /. z0) - (f /. x)).|| < r0 ) ) )
assume A10: 0 < r0 ; :: thesis: ex w1 being Real st
( 0 < w1 & ( for z0 being Real st z0 in dom f & |.(z0 - x).| < w1 holds
||.((f /. z0) - (f /. x)).|| < r0 ) )
then consider k being Nat such that
A11: for n being Nat
for x being set st n >= k & x in X holds
||.(((H . n) /. x) - (f /. x)).|| < r0 / 3 by A4, XREAL_1:222;
A12: ||.(((H . k) /. x) - (f /. x)).|| < r0 / 3 by A11, A3, A9;
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 consider h being continuous PartFunc of REAL,Y such that
A13: ( H . k = h & dom h = X ) by A2, Def2, A1;
A14: ( 0 < r0 / 3 & r0 / 3 is Real ) by A10, XREAL_1:222;
x in dom h by A9, A13, FUNCT_2:def 1;
then h is_continuous_in x by NFCONT_3:def 2;
then consider w1 being Real such that
A15: ( 0 < w1 & ( for x0 being Real st x0 in dom h & |.(x0 - x).| < w1 holds
||.((h /. x0) - (h /. x)).|| < r0 / 3 ) ) by A14, NFCONT_3:8;
take w1 = w1; :: thesis: ( 0 < w1 & ( for z0 being Real st z0 in dom f & |.(z0 - x).| < w1 holds
||.((f /. z0) - (f /. x)).|| < r0 ) )
thus 0 < w1 by A15; :: thesis: for z0 being Real st z0 in dom f & |.(z0 - x).| < w1 holds
||.((f /. z0) - (f /. x)).|| < r0
thus for z0 being Real st z0 in dom f & |.(z0 - x).| < w1 holds
||.((f /. z0) - (f /. x)).|| < r0 :: thesis: verum

proof

let z0 be Real; :: thesis: ( z0 in dom f & |.(z0 - x).| < w1 implies ||.((f /. z0) - (f /. x)).|| < r0 )
assume A16: ( z0 in dom f & |.(z0 - x).| < w1 ) ; :: thesis: ||.((f /. z0) - (f /. x)).|| < r0
then A17: z0 in dom h by FUNCT_2:def 1, A13;
then A18: ||.((h /. z0) - (h /. x)).|| < r0 / 3 by A16, A15;
A19: ||.((f /. x) - (h /. x)).|| < r0 / 3 by A12, A13, NORMSP_1:7;
||.((h /. z0) - (f /. z0)).|| < r0 / 3 by A17, A11, A13;
then ||.((f /. z0) - (h /. z0)).|| < r0 / 3 by NORMSP_1:7;
then ||.((f /. z0) - (h /. z0)).|| + ||.((f /. x) - (h /. x)).|| < (r0 / 3) + (r0 / 3) by A19, XREAL_1:8;
then A20: (||.((f /. z0) - (h /. z0)).|| + ||.((f /. x) - (h /. x)).||) + ||.((h /. z0) - (h /. x)).|| < ((r0 / 3) + (r0 / 3)) + (r0 / 3) by A18, XREAL_1:8;
(((f /. z0) - (h /. z0)) - ((f /. x) - (h /. x))) + ((h /. z0) - (h /. x)) = ((f /. z0) - (h /. z0)) - (((f /. x) - (h /. x)) - ((h /. z0) - (h /. x))) by RLVECT_1:29
.= ((f /. z0) - (h /. z0)) - ((f /. x) - ((h /. x) + ((h /. z0) - (h /. x)))) by RLVECT_1:27
.= ((f /. z0) - (h /. z0)) - ((f /. x) - ((h /. z0) - ((h /. x) - (h /. x)))) by RLVECT_1:29
.= ((f /. z0) - (h /. z0)) - ((f /. x) - ((h /. z0) - (0. Y))) by RLVECT_1:15
.= (f /. z0) - ((h /. z0) + ((f /. x) - (h /. z0))) by RLVECT_1:27
.= (f /. z0) - ((f /. x) - ((h /. z0) - (h /. z0))) by RLVECT_1:29
.= (f /. z0) - ((f /. x) - (0. Y)) by RLVECT_1:15
.= (f /. z0) - (f /. x) ;
then A21: ||.((f /. z0) - (f /. x)).|| <= ||.(((f /. z0) - (h /. z0)) - ((f /. x) - (h /. x))).|| + ||.((h /. z0) - (h /. x)).|| by NORMSP_1:def 1;
||.(((f /. z0) - (h /. z0)) - ((f /. x) - (h /. x))).|| + ||.((h /. z0) - (h /. x)).|| <= (||.((f /. z0) - (h /. z0)).|| + ||.((f /. x) - (h /. x)).||) + ||.((h /. z0) - (h /. x)).|| by XREAL_1:6, NORMSP_1:3;
then ||.((f /. z0) - (f /. x)).|| <= (||.((f /. z0) - (h /. z0)).|| + ||.((f /. x) - (h /. x)).||) + ||.((h /. z0) - (h /. x)).|| by A21, XXREAL_0:2;
hence ||.((f /. z0) - (f /. x)).|| < r0 by A20, XXREAL_0:2; :: thesis: verum

end;

end;

hence f is_continuous_in x by A9, NFCONT_3:8; :: thesis: verum

end;

then f is continuous by NFCONT_3:def 2;
hence lim seq in C by A3, Def2, A1; :: thesis: verum

end;

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