let X be set ; :: thesis: for H being Functional_Sequence of REAL,REAL st H is_unif_conv_on X & ( for n being Element of 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 Element of 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 Element of NAT holds (H . n) | X is continuous ; :: thesis: (lim (H,X)) | X is continuous
A3: H is_point_conv_on X by A1, Th23;
then A4: dom (lim (H,X)) = X by Def14;
A5: X common_on_dom H by A1, Def13;
for x0 being real number st x0 in dom ((lim (H,X)) | X) holds
(lim (H,X)) | X is_continuous_in x0

proof

let x0 be real number ; :: 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 Real by XREAL_0:def 1;
for r being real number st 0 < r holds
ex s being real number st
( 0 < s & ( for x1 being real number st x1 in dom ((lim (H,X)) | X) & abs (x1 - x0) < s holds
abs ((((lim (H,X)) | X) . x1) - (((lim (H,X)) | X) . x0)) < r ) )

proof

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