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 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 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 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 :: thesis: for p being Point of T holds l is_continuous_at p

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

now :: thesis: for e being Real st e > 0 holds
ex H being Subset of T st
( H is open & p in H & ( for y being Point of T st y in H holds
|.((l . y) - (l . p)).| < e ) )

let e be Real; :: 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
|.((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
|.((l . y) - (l . p)).| < e ) )
reconsider e3 = e / 3 as Real ;
A4: e3 > 0 by A3, XREAL_1:139;
then consider k being Nat such that
A5: for n being Nat
for x being Point of T st n >= k & x in the carrier of T holds
|.(((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: |.((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
|.((Fk . y) - (Fk . p)).| < e3 by A4, Th19;
take H = H; :: thesis: ( H is open & p in H & ( for y being Point of T st y in H holds
|.((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
|.((l . y) - (l . p)).| < e
let y be Point of T; :: thesis: ( y in H implies |.((l . y) - (l . p)).| < e )
assume A9: y in H ; :: thesis: |.((l . y) - (l . p)).| < e
|.((Fk . y) - (l . y)).| < e3 by A5;
then |.(- ((Fk . y) - (l . y))).| < e3 by COMPLEX1:52;
then ( |.(((Fk . p) - (l . p)) + ((- (Fk . y)) + (l . y))).| <= |.((Fk . p) - (l . p)).| + |.(- ((Fk . y) - (l . y))).| & |.((Fk . p) - (l . p)).| + |.(- ((Fk . y) - (l . y))).| < e3 + e3 ) by A6, COMPLEX1:56, XREAL_1:8;
then |.(((Fk . p) - (l . p)) + ((- (Fk . y)) + (l . y))).| < 2 * e3 by XXREAL_0:2;
then ( |.(((Fk . y) - (Fk . p)) + (((Fk . p) - (l . p)) + ((- (Fk . y)) + (l . y)))).| <= |.((Fk . y) - (Fk . p)).| + |.(((Fk . p) - (l . p)) + ((- (Fk . y)) + (l . y))).| & |.((Fk . y) - (Fk . p)).| + |.(((Fk . p) - (l . p)) + ((- (Fk . y)) + (l . y))).| < e3 + (2 * e3) ) by A8, A9, COMPLEX1:56, XREAL_1:8;
hence |.((l . y) - (l . p)).| < e by XXREAL_0:2; :: thesis: verum

end;

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

end;

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