let T be non empty TopSpace; 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; ( 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
; 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 for p being Point of T holds l is_continuous_at plet p be
Point of
T;
l is_continuous_at pnow 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;
( 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
;
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;
( 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;
for y being Point of T st y in H holds
|.((l . y) - (l . p)).| < elet y be
Point of
T;
( y in H implies |.((l . y) - (l . p)).| < e )assume A9:
y in H
;
|.((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;
verum end; hence
l is_continuous_at p
by Th19;
verum end;
hence
lim (F, the carrier of T) is continuous Function of T,R^1
by TMAP_1:44; verum