let T be non empty TopSpace; :: thesis: for F being Functional_Sequence of the carrier of T,REAL st F is_unif_conv_on the carrier of T & ( for i being Element of NAT holds F . i is continuous Function of T,R^1 ) holds
lim (F, the carrier of T) is continuous Function of T,R^1
let F be Functional_Sequence of the carrier of T,REAL; :: thesis: ( F is_unif_conv_on the carrier of T & ( for i being Element of NAT holds F . i is continuous Function of T,R^1 ) implies lim (F, the carrier of T) is continuous Function of T,R^1 )
assume that
A1: F is_unif_conv_on the carrier of T and
A2: for i being Element of NAT holds F . i is continuous Function of T,R^1 ; :: thesis: lim (F, the carrier of T) is continuous Function of T,R^1
F is_point_conv_on the carrier of T by A1, SEQFUNC:43;
then dom (lim (F, the carrier of T)) = the carrier of T by SEQFUNC:def 13;
then reconsider l = lim (F, the carrier of T) as Function of T,R^1 by FUNCT_2:def 1, TOPMETR:17;

now

let p be Point of T; :: thesis: l is_continuous_at p

now

let e be real number ; :: thesis: ( e > 0 implies ex H being Subset of T st
( H is open & p in H & ( for y being Point of T st y in H holds
abs ((l . y) - (l . p)) < e ) ) )
assume A3: e > 0 ; :: thesis: ex H being Subset of T st
( H is open & p in H & ( for y being Point of T st y in H holds
abs ((l . y) - (l . p)) < e ) )
reconsider e3 = e / 3 as Real ;
A4: e3 > 0 by A3, XREAL_1:139;
then consider k being Element of NAT such that
A5: for n being Element of NAT
for x being Point of T st n >= k & x in the carrier of T holds
abs (((F . n) . x) - ((lim (F, the carrier of T)) . x)) < e3 by A1, SEQFUNC:43;
reconsider Fk = F . k as continuous Function of T,R^1 by A2;
A6: abs ((Fk . p) - (l . p)) < e3 by A5;
Fk is_continuous_at p by TMAP_1:44;
then consider H being Subset of T such that
A7: ( H is open & p in H ) and
A8: for y being Point of T st y in H holds
abs ((Fk . y) - (Fk . p)) < e3 by A4, Th21;
take H = H; :: thesis: ( H is open & p in H & ( for y being Point of T st y in H holds
abs ((l . y) - (l . p)) < e ) )
thus ( H is open & p in H ) by A7; :: thesis: for y being Point of T st y in H holds
abs ((l . y) - (l . p)) < e
let y be Point of T; :: thesis: ( y in H implies abs ((l . y) - (l . p)) < e )
assume A9: y in H ; :: thesis: abs ((l . y) - (l . p)) < e
abs ((Fk . y) - (l . y)) < e3 by A5;
then abs (- ((Fk . y) - (l . y))) < e3 by COMPLEX1:52;
then ( abs (((Fk . p) - (l . p)) + ((- (Fk . y)) + (l . y))) <= (abs ((Fk . p) - (l . p))) + (abs (- ((Fk . y) - (l . y)))) & (abs ((Fk . p) - (l . p))) + (abs (- ((Fk . y) - (l . y)))) < e3 + e3 ) by A6, COMPLEX1:56, XREAL_1:8;
then abs (((Fk . p) - (l . p)) + ((- (Fk . y)) + (l . y))) < 2 * e3 by XXREAL_0:2;
then ( abs (((Fk . y) - (Fk . p)) + (((Fk . p) - (l . p)) + ((- (Fk . y)) + (l . y)))) <= (abs ((Fk . y) - (Fk . p))) + (abs (((Fk . p) - (l . p)) + ((- (Fk . y)) + (l . y)))) & (abs ((Fk . y) - (Fk . p))) + (abs (((Fk . p) - (l . p)) + ((- (Fk . y)) + (l . y)))) < e3 + (2 * e3) ) by A8, A9, COMPLEX1:56, XREAL_1:8;
hence abs ((l . y) - (l . p)) < e by XXREAL_0:2; :: thesis: verum

end;

hence l is_continuous_at p by Th21; :: thesis: verum

end;

hence lim (F, the carrier of T) is continuous Function of T,R^1 by TMAP_1:44; :: thesis: verum