let X be set ; :: thesis: for H being Functional_Sequence of REAL,REAL st H is_unif_conv_on X & ( for n being Nat holds (H . n) | X is continuous ) holds
(lim (H,X)) | X is continuous
let H be Functional_Sequence of REAL,REAL; :: thesis: ( H is_unif_conv_on X & ( for n being Nat holds (H . n) | X is continuous ) implies (lim (H,X)) | X is continuous )
set l = lim (H,X);
assume that
A1: H is_unif_conv_on X and
A2: for n being Nat holds (H . n) | X is continuous ; :: thesis: (lim (H,X)) | X is continuous
A3: H is_point_conv_on X by A1, Th21;
then A4: dom (lim (H,X)) = X by Def13;
A5: X common_on_dom H by A1;
for x0 being Real st x0 in dom ((lim (H,X)) | X) holds
(lim (H,X)) | X is_continuous_in x0

proof

let x0 be Real; :: thesis: ( x0 in dom ((lim (H,X)) | X) implies (lim (H,X)) | X is_continuous_in x0 )
assume x0 in dom ((lim (H,X)) | X) ; :: thesis: (lim (H,X)) | X is_continuous_in x0
then A6: x0 in X by RELAT_1:57;
reconsider x0 = x0 as Element of REAL by XREAL_0:def 1;
for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Real st x1 in dom ((lim (H,X)) | X) & |.(x1 - x0).| < s holds
|.((((lim (H,X)) | X) . x1) - (((lim (H,X)) | X) . x0)).| < r ) )

proof

let r be Real; :: thesis: ( 0 < r implies ex s being Real st
( 0 < s & ( for x1 being Real st x1 in dom ((lim (H,X)) | X) & |.(x1 - x0).| < s holds
|.((((lim (H,X)) | X) . x1) - (((lim (H,X)) | X) . x0)).| < r ) ) )
assume 0 < r ; :: thesis: ex s being Real st
( 0 < s & ( for x1 being Real st x1 in dom ((lim (H,X)) | X) & |.(x1 - x0).| < s holds
|.((((lim (H,X)) | X) . x1) - (((lim (H,X)) | X) . x0)).| < r ) )
then A7: 0 < r / 3 by XREAL_1:222;
reconsider r = r as Element of REAL by XREAL_0:def 1;
consider k being Nat such that
A8: for n being Nat
for x1 being Element of REAL st n >= k & x1 in X holds
|.(((H . n) . x1) - ((lim (H,X)) . x1)).| < r / 3 by A1, A7, Th42;
consider k1 being Nat such that
A9: for n being Nat st n >= k1 holds
|.(((H . n) . x0) - ((lim (H,X)) . x0)).| < r / 3 by A3, A6, A7, Th20;
reconsider m = max (k,k1) as Nat by TARSKI:1;
set h = H . m;
A10: X c= dom (H . m) by A5;
A11: dom ((H . m) | X) = (dom (H . m)) /\ X by RELAT_1:61
.= X by A10, XBOOLE_1:28 ;
(H . m) | X is continuous by A2;
then (H . m) | X is_continuous_in x0 by A6, A11, FCONT_1:def 2;
then consider s being Real such that
A12: 0 < s and
A13: for x1 being Real st x1 in dom ((H . m) | X) & |.(x1 - x0).| < s holds
|.((((H . m) | X) . x1) - (((H . m) | X) . x0)).| < r / 3 by A7, FCONT_1:3;
reconsider s = s as Real ;
take s ; :: thesis: ( 0 < s & ( for x1 being Real st x1 in dom ((lim (H,X)) | X) & |.(x1 - x0).| < s holds
|.((((lim (H,X)) | X) . x1) - (((lim (H,X)) | X) . x0)).| < r ) )
thus 0 < s by A12; :: thesis: for x1 being Real st x1 in dom ((lim (H,X)) | X) & |.(x1 - x0).| < s holds
|.((((lim (H,X)) | X) . x1) - (((lim (H,X)) | X) . x0)).| < r
let x1 be Real; :: thesis: ( x1 in dom ((lim (H,X)) | X) & |.(x1 - x0).| < s implies |.((((lim (H,X)) | X) . x1) - (((lim (H,X)) | X) . x0)).| < r )
assume that
A14: x1 in dom ((lim (H,X)) | X) and
A15: |.(x1 - x0).| < s ; :: thesis: |.((((lim (H,X)) | X) . x1) - (((lim (H,X)) | X) . x0)).| < r
A16: dom ((lim (H,X)) | X) = (dom (lim (H,X))) /\ X by RELAT_1:61
.= X by A4 ;
then |.((((H . m) | X) . x1) - (((H . m) | X) . x0)).| < r / 3 by A11, A13, A14, A15;
then |.(((H . m) . x1) - (((H . m) | X) . x0)).| < r / 3 by A16, A11, A14, FUNCT_1:47;
then A17: |.(((H . m) . x1) - ((H . m) . x0)).| < r / 3 by A6, FUNCT_1:49;
|.(((H . m) . x0) - ((lim (H,X)) . x0)).| < r / 3 by A9, XXREAL_0:25;
then ( |.((((H . m) . x1) - ((H . m) . x0)) + (((H . m) . x0) - ((lim (H,X)) . x0))).| <= |.(((H . m) . x1) - ((H . m) . x0)).| + |.(((H . m) . x0) - ((lim (H,X)) . x0)).| & |.(((H . m) . x1) - ((H . m) . x0)).| + |.(((H . m) . x0) - ((lim (H,X)) . x0)).| < (r / 3) + (r / 3) ) by A17, COMPLEX1:56, XREAL_1:8;
then A18: |.((((H . m) . x1) - ((H . m) . x0)) + (((H . m) . x0) - ((lim (H,X)) . x0))).| < (r / 3) + (r / 3) by XXREAL_0:2;
|.(((lim (H,X)) . x1) - ((lim (H,X)) . x0)).| = |.((((lim (H,X)) . x1) - ((H . m) . x1)) + ((((H . m) . x1) - ((H . m) . x0)) + (((H . m) . x0) - ((lim (H,X)) . x0)))).| ;
then A19: |.(((lim (H,X)) . x1) - ((lim (H,X)) . x0)).| <= |.(((lim (H,X)) . x1) - ((H . m) . x1)).| + |.((((H . m) . x1) - ((H . m) . x0)) + (((H . m) . x0) - ((lim (H,X)) . x0))).| by COMPLEX1:56;
|.(((H . m) . x1) - ((lim (H,X)) . x1)).| < r / 3 by A8, A16, A14, XXREAL_0:25;
then |.(- (((lim (H,X)) . x1) - ((H . m) . x1))).| < r / 3 ;
then |.(((lim (H,X)) . x1) - ((H . m) . x1)).| < r / 3 by COMPLEX1:52;
then |.(((lim (H,X)) . x1) - ((H . m) . x1)).| + |.((((H . m) . x1) - ((H . m) . x0)) + (((H . m) . x0) - ((lim (H,X)) . x0))).| < (r / 3) + ((r / 3) + (r / 3)) by A18, XREAL_1:8;
then |.(((lim (H,X)) . x1) - ((lim (H,X)) . x0)).| < ((r / 3) + (r / 3)) + (r / 3) by A19, XXREAL_0:2;
then |.((((lim (H,X)) | X) . x1) - ((lim (H,X)) . x0)).| < r by A14, FUNCT_1:47;
hence |.((((lim (H,X)) | X) . x1) - (((lim (H,X)) | X) . x0)).| < r by A4, RELAT_1:68; :: thesis: verum

end;

hence (lim (H,X)) | X is_continuous_in x0 by FCONT_1:3; :: thesis: verum

end;

hence (lim (H,X)) | X is continuous by FCONT_1:def 2; :: thesis: verum