let G be a_neighborhood of LimH . x; :: thesis: ex H being a_neighborhood of x st LimH .: H c= G
consider r being Real such that
A5: ( r > 0 & { y where y is Point of T : ||.(y - (LimH . x)).|| < r } c= G ) by Th30;
A6: 0 < r / 3 by XREAL_1:222, A5;
reconsider r = r as Element of REAL by XREAL_0:def 1;
consider k being Nat such that
A7: for n being Nat
for x1 being Element of S st n >= k & x1 in the carrier of S holds
||.(((H . n) /. x1) - (LimH /. x1)).|| < r / 3 by A1, XREAL_1:222, A5, A3, SEQFUNC2:33;
consider k1 being Nat such that
A8: for n being Nat st n >= k1 holds
||.(((H . n) /. x) - (LimH /. x)).|| < r / 3 by A4, A6, A3, SEQFUNC2:11;
reconsider m = max (k,k1) as Nat by XXREAL_0:def 10;
consider h being Function of S,T such that
A9: ( h = H . m & h is continuous ) by A2;
set W = { y where y is Point of T : ||.(y - (h . x)).|| < r / 3 } ;
then reconsider W = { y where y is Point of T : ||.(y - (h . x)).|| < r / 3 } as Subset of T by TARSKI:def 3;
W is a_neighborhood of h . x by XREAL_1:222, A5, Th30;
then consider H being a_neighborhood of x such that
A10: h .: H c= W by A9, TMAP_1:44, TMAP_1:def 2;
take H ; :: thesis: LimH .: H c= G
hence LimH .: H c= G ; :: thesis: verum