0 ex k st for n,x st n>= k & x in X holds |.(H.n).x-f
.x .|0;
then consider k such that
A6: for n,x st n>=k & x in X holds |.(H.n).x-f.x.|

=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=k & x in X holds |.(H.n).x-(
lim(H,X)).x.|=k & x1 in X
holds |.(H.n).x1-l.x1.|=k1 holds |.(H.n).x0 - l.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 by A5;
A11: dom(h|X) = dom h /\ X by RELAT_1:61
.= X by A10,XBOOLE_1:28;
h|X is continuous by A2;
then h|X is_continuous_in x0 by A6,A11,FCONT_1:def 2;
then consider s be Real such that
A12: 0