let S be non empty TopSpace; :: thesis: for T being NormedLinearTopSpace
for H being Functional_Sequence of the carrier of S, the carrier of T
for LimH being Function of S,T st H is_unif_conv_on the carrier of S & ( for n being Nat ex Hn being Function of S,T st
( Hn = H . n & Hn is continuous ) ) & LimH = lim (H, the carrier of S) holds
LimH is continuous
let T be NormedLinearTopSpace; :: thesis: for H being Functional_Sequence of the carrier of S, the carrier of T
for LimH being Function of S,T st H is_unif_conv_on the carrier of S & ( for n being Nat ex Hn being Function of S,T st
( Hn = H . n & Hn is continuous ) ) & LimH = lim (H, the carrier of S) holds
LimH is continuous
let H be Functional_Sequence of the carrier of S, the carrier of T; :: thesis: for LimH being Function of S,T st H is_unif_conv_on the carrier of S & ( for n being Nat ex Hn being Function of S,T st
( Hn = H . n & Hn is continuous ) ) & LimH = lim (H, the carrier of S) holds
LimH is continuous
let LimH be Function of S,T; :: thesis: ( H is_unif_conv_on the carrier of S & ( for n being Nat ex Hn being Function of S,T st
( Hn = H . n & Hn is continuous ) ) & LimH = lim (H, the carrier of S) implies LimH is continuous )
assume that
A1: H is_unif_conv_on the carrier of S and
A2: for n being Nat ex Hn being Function of S,T st
( Hn = H . n & Hn is continuous ) and
A3: LimH = lim (H, the carrier of S) ; :: thesis: LimH is continuous
set X = the carrier of S;
A4: H is_point_conv_on the carrier of S by A1, SEQFUNC2:33;
for x being Point of S holds LimH is_continuous_at x

proof

let x be Point of S; :: thesis: LimH is_continuous_at x
for G being a_neighborhood of LimH . x ex H being a_neighborhood of x st LimH .: H c= G

proof

let G be a_neighborhood of LimH . x; :: thesis: ex H being a_neighborhood of x st LimH .: H c= G
consider r being Real such that
A5: ( r > 0 & { y where y is Point of T : ||.(y - (LimH . x)).|| < r } c= G ) by Th30;
A6: 0 < r / 3 by XREAL_1:222, A5;
reconsider r = r as Element of REAL by XREAL_0:def 1;
consider k being Nat such that
A7: for n being Nat
for x1 being Element of S st n >= k & x1 in the carrier of S holds
||.(((H . n) /. x1) - (LimH /. x1)).|| < r / 3 by A1, XREAL_1:222, A5, A3, SEQFUNC2:33;
consider k1 being Nat such that
A8: for n being Nat st n >= k1 holds
||.(((H . n) /. x) - (LimH /. x)).|| < r / 3 by A4, A6, A3, SEQFUNC2:11;
reconsider m = max (k,k1) as Nat by XXREAL_0:def 10;
consider h being Function of S,T such that
A9: ( h = H . m & h is continuous ) by A2;
set W = { y where y is Point of T : ||.(y - (h . x)).|| < r / 3 } ;

now :: thesis: for z being object st z in { y where y is Point of T : ||.(y - (h . x)).|| < r / 3 } holds
z in the carrier of T

let z be object ; :: thesis: ( z in { y where y is Point of T : ||.(y - (h . x)).|| < r / 3 } implies z in the carrier of T )
assume z in { y where y is Point of T : ||.(y - (h . x)).|| < r / 3 } ; :: thesis: z in the carrier of T
then ex y being Point of T st
( z = y & ||.(y - (h . x)).|| < r / 3 ) ;
hence z in the carrier of T ; :: thesis: verum

end;

then reconsider W = { y where y is Point of T : ||.(y - (h . x)).|| < r / 3 } as Subset of T by TARSKI:def 3;
W is a_neighborhood of h . x by XREAL_1:222, A5, Th30;
then consider H being a_neighborhood of x such that
A10: h .: H c= W by A9, TMAP_1:44, TMAP_1:def 2;
take H ; :: thesis: LimH .: H c= G

now :: thesis: for z being object st z in LimH .: H holds
z in G

let z be object ; :: thesis: ( z in LimH .: H implies z in G )
assume z in LimH .: H ; :: thesis: z in G
then consider s being object such that
A11: ( s in the carrier of S & s in H & z = LimH . s ) by FUNCT_2:64;
reconsider s = s as Point of S by A11;
h . s in h .: H by A11, FUNCT_2:35;
then h . s in W by A10;
then A12: ex y being Point of T st
( y = h . s & ||.(y - (h . x)).|| < r / 3 ) ;
||.((h /. s) - (LimH /. s)).|| < r / 3 by A7, A9, XXREAL_0:25;
then A13: ||.((LimH /. s) - (h /. s)).|| < r / 3 by NORMSP_1:7;
A14: ||.((h /. x) - (LimH /. x)).|| < r / 3 by A8, A9, XXREAL_0:25;
(LimH . s) - (LimH . x) = (((LimH . s) - (h /. s)) + (h /. s)) - (LimH . x) by RLVECT_4:1
.= ((LimH . s) - (h /. s)) + ((h /. s) - (LimH . x)) by RLVECT_1:28
.= ((LimH . s) - (h /. s)) + ((((h /. s) - (h /. x)) + (h /. x)) - (LimH . x)) by RLVECT_4:1
.= ((LimH . s) - (h /. s)) + (((h /. s) - (h /. x)) + ((h /. x) - (LimH . x))) by RLVECT_1:28 ;
then A15: ||.((LimH . s) - (LimH . x)).|| <= ||.((LimH . s) - (h /. s)).|| + ||.(((h /. s) - (h /. x)) + ((h /. x) - (LimH . x))).|| by NORMSP_1:def 1;
A16: ||.((LimH . s) - (h /. s)).|| + ||.(((h /. s) - (h /. x)) + ((h /. x) - (LimH . x))).|| < (r / 3) + ||.(((h /. s) - (h /. x)) + ((h /. x) - (LimH . x))).|| by XREAL_1:8, A13;
A17: ||.(((h /. s) - (h /. x)) + ((h /. x) - (LimH . x))).|| <= ||.((h /. s) - (h /. x)).|| + ||.((h /. x) - (LimH . x)).|| by NORMSP_1:def 1;
||.((h /. s) - (h /. x)).|| + ||.((h /. x) - (LimH . x)).|| < (r / 3) + (r / 3) by XREAL_1:8, A12, A14;
then ||.(((h /. s) - (h /. x)) + ((h /. x) - (LimH . x))).|| < (r / 3) + (r / 3) by A17, XXREAL_0:2;
then (r / 3) + ||.(((h /. s) - (h /. x)) + ((h /. x) - (LimH . x))).|| < (r / 3) + ((r / 3) + (r / 3)) by XREAL_1:8;
then ||.((LimH . s) - (h /. s)).|| + ||.(((h /. s) - (h /. x)) + ((h /. x) - (LimH . x))).|| < r by A16, XXREAL_0:2;
then ||.((LimH . s) - (LimH . x)).|| < r by A15, XXREAL_0:2;
then LimH . s in { y where y is Point of T : ||.(y - (LimH . x)).|| < r } ;
hence z in G by A11, A5; :: thesis: verum

end;

hence LimH .: H c= G ; :: thesis: verum

end;

hence LimH is_continuous_at x by TMAP_1:def 2; :: thesis: verum

end;

hence LimH is continuous by TMAP_1:44; :: thesis: verum