0 ex k st for n,x st n>= k & x in X
holds ||.(H.n)/.x-f/.x .|| < p;
thus X common_on_dom H by A1;
A4:
now
let x such that
A5: x in X;
let p;
assume p>0;
then consider k such that
A6: for n, x st n >= k & x in X holds ||.(H.n)/.x-f/.x.|| < p by A3;
take k;
let n;
assume n >= k;
hence ||.(H.n)/.x-f/.x.|| 0;
then consider k such that
A8: for n,x st n>=k & x in X holds ||.(H.n)/.x-f/.x.||= k & x in X;
hence thesis by A7, A8;
end;
assume that
A9: X common_on_dom H and
A10: H is_point_conv_on X and
A11: for r st 0 < r ex k st for n, x st n >= k & x in X
holds ||.(H.n)/.x-(lim(H, X))/.x.|| < r;
dom lim(H, X) = X by A10, Def13;
hence thesis by A9, A11;
end;
reserve
V, W for RealNormSpace,
H for Functional_Sequence of the carrier of V,the carrier of W;
theorem
H is_unif_conv_on X & (for n holds (H.n)|X is_continuous_on X)
implies lim(H, X) is_continuous_on X
proof
set l = lim(H, X);
assume that
A1: H is_unif_conv_on X and
A2: for n holds (H.n)|X is_continuous_on X;
A3: H is_point_conv_on X by A1, Th21;
then
A4: dom l = X by Def13;
A5: X common_on_dom H by A1;
for x0 be Point of V st x0 in X holds l|X is_continuous_in x0
proof
let x0 be Point of V;
assume
A6: x0 in X; then
A60: x0 in dom(l|X) by RELAT_1:62, A4;
for r be Real st 0 < r ex s be Real st 0 < s
& for x1 be Point of V st x1 in dom (l|X)
& ||.x1-x0.|| < s holds ||.(l|X)/.x1-(l|X)/.x0.|| < r
proof
let r be Real;
assume
A7: 0 < r;
reconsider r as Element of REAL by XREAL_0:def 1;
consider k such that
A8: for n for x1 being Element of V st n>=k & x1 in X
holds ||.(H.n)/.x1-l/.x1.||=k1 holds ||.(H.n)/.x0 - l/.x0.|| < r/3 by A3, A6, Th20;
reconsider m = max(k,k1) as Nat by TARSKI:1;
set h = H.m;
A11: dom(h|X) = dom h /\ X by RELAT_1:61
.= X by A5, XBOOLE_1:28;
h|X is_continuous_on X by A2;
then h is_continuous_on X by NFCONT_1:21;
then h|X is_continuous_in x0 by A6, NFCONT_1:def 7;
then consider s be Real such that
A12: 0