let X be set ; :: thesis: for V, W being RealNormSpace
for H being Functional_Sequence of the carrier of V, the carrier of W st H is_unif_conv_on X & ( for n being Nat holds (H . n) | X is_continuous_on X ) holds
lim (H,X) is_continuous_on X
let V, W be RealNormSpace; :: thesis: for H being Functional_Sequence of the carrier of V, the carrier of W st H is_unif_conv_on X & ( for n being Nat holds (H . n) | X is_continuous_on X ) holds
lim (H,X) is_continuous_on X
let H be Functional_Sequence of the carrier of V, the carrier of W; :: thesis: ( H is_unif_conv_on X & ( for n being Nat holds (H . n) | X is_continuous_on X ) implies lim (H,X) is_continuous_on X )
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_on X ; :: thesis: lim (H,X) is_continuous_on X
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 Point of V st x0 in X holds
(lim (H,X)) | X is_continuous_in x0

proof

let x0 be Point of V; :: thesis: ( x0 in X implies (lim (H,X)) | X is_continuous_in x0 )
assume A6: x0 in X ; :: thesis: (lim (H,X)) | X is_continuous_in x0
then A60: x0 in dom ((lim (H,X)) | X) by RELAT_1:62, A4;
for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Point of V 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 Point of V st x1 in dom ((lim (H,X)) | X) & ||.(x1 - x0).|| < s holds
||.((((lim (H,X)) | X) /. x1) - (((lim (H,X)) | X) /. x0)).|| < r ) ) )
assume A7: 0 < r ; :: thesis: ex s being Real st
( 0 < s & ( for x1 being Point of V st x1 in dom ((lim (H,X)) | X) & ||.(x1 - x0).|| < s holds
||.((((lim (H,X)) | X) /. x1) - (((lim (H,X)) | X) /. x0)).|| < r ) )
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 V st n >= k & x1 in X holds
||.(((H . n) /. x1) - ((lim (H,X)) /. x1)).|| < r / 3 by A1, A7, XREAL_1:222, Th42;
0 < r / 3 by A7, XREAL_1:222;
then 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, Th20;
reconsider m = max (k,k1) as Nat by TARSKI:1;
set h = H . m;
A11: dom ((H . m) | X) = (dom (H . m)) /\ X by RELAT_1:61
.= X by A5, XBOOLE_1:28 ;
(H . m) | X is_continuous_on X by A2;
then H . m is_continuous_on X by NFCONT_1:21;
then (H . m) | X is_continuous_in x0 by A6, NFCONT_1:def 7;
then consider s being Real such that
A12: 0 < s and
A13: for x1 being Point of V st x1 in dom ((H . m) | X) & ||.(x1 - x0).|| < s holds
||.((((H . m) | X) /. x1) - (((H . m) | X) /. x0)).|| < r / 3 by A7, XREAL_1:222, NFCONT_1:7;
take s ; :: thesis: ( 0 < s & ( for x1 being Point of V 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 Point of V 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 Point of V; :: 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, PARTFUN1:80;
then A17: ||.(((H . m) /. x1) - ((H . m) /. x0)).|| < r / 3 by A11, A6, PARTFUN1:80;
||.(((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, NORMSP_1:def 1, 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)) - ((lim (H,X)) /. x0)).|| by RLVECT_4:1
.= ||.((((lim (H,X)) /. x1) - ((H . m) /. x1)) + (((H . m) /. x1) - ((lim (H,X)) /. x0))).|| by RLVECT_1:28
.= ||.((((lim (H,X)) /. x1) - ((H . m) /. x1)) + (((((H . m) /. x1) - ((H . m) /. x0)) + ((H . m) /. x0)) - ((lim (H,X)) /. x0))).|| by RLVECT_4:1
.= ||.((((lim (H,X)) /. x1) - ((H . m) /. x1)) + ((((H . m) /. x1) - ((H . m) /. x0)) + (((H . m) /. x0) - ((lim (H,X)) /. x0)))).|| by RLVECT_1:28 ;
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 NORMSP_1:def 1;
||.(((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 by RLVECT_1:33;
then ||.(((lim (H,X)) /. x1) - ((H . m) /. x1)).|| < r / 3 by NORMSP_1:2;
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, PARTFUN1:80;
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 NFCONT_1:7, A60; :: thesis: verum

end;

hence lim (H,X) is_continuous_on X by NFCONT_1:def 7, A4; :: thesis: verum