let T, T1 be non empty TopSpace; :: thesis: for F being Function of the carrier of T,(Funcs ( the carrier of T, the carrier of T1)) st ( for p being Point of T holds F . p is continuous Function of T,T1 ) holds
for S being Function of the carrier of T,(bool the carrier of T) st ( 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 ) ) ) holds
F Toler is continuous
let F be Function of the carrier of T,(Funcs ( the carrier of T, the carrier of T1)); :: thesis: ( ( for p being Point of T holds F . p is continuous Function of T,T1 ) implies for S being Function of the carrier of T,(bool the carrier of T) st ( 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 ) ) ) holds
F Toler is continuous )
assume A1: for p being Point of T holds F . p is continuous Function of T,T1 ; :: thesis: for S being Function of the carrier of T,(bool the carrier of T) st ( 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 ) ) ) holds
F Toler is continuous
let S be Function of the carrier of T,(bool the carrier of T); :: thesis: ( ( 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 ) ) ) implies F Toler is continuous )
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: F Toler is continuous

now :: thesis: for t being Point of T holds F Toler is_continuous_at t

let t be Point of T; :: thesis: F Toler is_continuous_at t
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 )

proof

reconsider Ft = F . t as Function of T,T1 by A1;
let R be Subset of T1; :: thesis: ( R is open & (F Toler) . t in R implies ex H being Subset of T st
( H is open & t in H & (F Toler) .: H c= R ) )
assume that
A3: R is open and
A4: (F Toler) . t in R ; :: thesis: ex H being Subset of T st
( H is open & t in H & (F Toler) .: H c= R )
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

proof

let FSh be object ; :: according to TARSKI:def 3 :: thesis: ( not FSh in (F Toler) .: (A /\ (S . t)) or FSh in R )
assume FSh in (F Toler) .: (A /\ (S . t)) ; :: thesis: FSh in R
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: verum

end;

take A /\ (S . t) ; :: thesis: ( A /\ (S . t) is open & t in A /\ (S . t) & (F Toler) .: (A /\ (S . t)) c= R )
( 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: verum

end;

hence F Toler is_continuous_at t by TMAP_1:43; :: thesis: verum

end;

hence F Toler is continuous by TMAP_1:50; :: thesis: verum