let T, T1 be non empty TopSpace; :: thesis:
let F be Function of the carrier of T,(Funcs ( the carrier of T, the carrier of T1)); :: thesis:
assume A1: for p being Point of T holds F . p is continuous Function of T,T1 ; :: thesis:
let S be Function of the carrier of T,(bool the carrier of T); :: thesis:
assume A2: for p being Point of T holds
( p in S . p & S . p is open & ( for p, q being Point of T st p in S . q holds
(F . p) . p = (F . q) . p ) ) ; :: thesis:

let t be Point of T; :: thesis:
for R being Subset of T1 st R is open & (F Toler) . t in R holds
ex H being Subset of T st
( H is open & t in H & (F Toler) .: H c= R )

reconsider Ft = F . t as Function of T,T1 by A1;
let R be Subset of T1; :: thesis:
assume that
A3: R is open and
A4: (F Toler) . t in R ; :: thesis:
Ft is continuous by A1;
then A5: Ft is_continuous_at t by TMAP_1:50;
Ft . t in R by A4, Def8;
then consider A being Subset of T such that
A6: ( A is open & t in A ) and
A7: Ft .: A c= R by A3, A5, TMAP_1:43;
set H = A /\ (S . t);
A8: (F Toler) .: (A /\ (S . t)) c= R

let FSh be object ; :: according to TARSKI:def 3 :: thesis:
assume FSh in (F Toler) .: (A /\ (S . t)) ; :: thesis:
then consider h being object such that
A9: h in dom (F Toler) and
A10: h in A /\ (S . t) and
A11: FSh = (F Toler) . h by FUNCT_1:def 6;
reconsider h9 = h as Point of T by A9;
( h9 in S . t & FSh = (F . h9) . h9 ) by A10, A11, Def8, XBOOLE_0:def 4;
then A12: FSh = Ft . h9 by A2;
A13: the carrier of T = dom Ft by FUNCT_2:def 1;
h9 in A by A10, XBOOLE_0:def 4;
then FSh in Ft .: A by A12, A13, FUNCT_1:def 6;
hence FSh in R by A7; :: thesis:

end;

take A /\ (S . t) ; :: thesis:
( S . t is open & t in S . t ) by A2;
hence ( A /\ (S . t) is open & t in A /\ (S . t) & (F Toler) .: (A /\ (S . t)) c= R ) by A6, A8, XBOOLE_0:def 4; :: thesis:

end;

end;