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 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 holds
( p in S . p & S . p is open & ( for p, q being Point of 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 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 holds
( p in S . p & S . p is open & ( for p, q being Point of st p in S . q holds
(F . p) . p = (F . q) . p ) ) ) holds
F Toler is continuous )
assume A1: for p being Point of 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 holds
( p in S . p & S . p is open & ( for p, q being Point of 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 holds
( p in S . p & S . p is open & ( for p, q being Point of st p in S . q holds
(F . p) . p = (F . q) . p ) ) ) implies F Toler is continuous )
assume A2: for p being Point of holds
( p in S . p & S . p is open & ( for p, q being Point of st p in S . q holds
(F . p) . p = (F . q) . p ) ) ; :: thesis: F Toler is continuous

now

let t be Point of ; :: thesis: F Toler is_continuous_at t
for R being Subset of st R is open & (F Toler ) . t in R holds
ex H being Subset of 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 ; :: thesis: ( R is open & (F Toler ) . t in R implies ex H being Subset of 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 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:55;
Ft . t in R by A4, Def8;
then consider A being Subset of such that
A6: ( A is open & t in A ) and
A7: Ft .: A c= R by A3, A5, TMAP_1:48;
set H = A /\ (S . t);
A8: (F Toler ) .: (A /\ (S . t)) c= R

proof

let FSh be set ; :: 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 set 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 12;
reconsider h' = h as Point of by A9;
( h' in S . t & FSh = (F . h') . h' ) by A10, A11, Def8, XBOOLE_0:def 4;
then A12: FSh = Ft . h' by A2;
A13: the carrier of T = dom Ft by FUNCT_2:def 1;
h' in A by A10, XBOOLE_0:def 4;
then FSh in Ft .: A by A12, A13, FUNCT_1:def 12;
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:48; :: thesis: verum

end;

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