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

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

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 A3: ( R is open & (F Toler ) . t in R ) ; :: thesis: 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;
Ft is continuous by A1;
then ( Ft is_continuous_at t & Ft . t in R ) by A3, Def8, TMAP_1:55;
then consider A being Subset of T such that
A4: ( A is open & t in A & Ft .: A c= R ) by A3, TMAP_1:48;
set H = A /\ (S . t);
take A /\ (S . t) ; :: thesis: ( A /\ (S . t) is open & t in A /\ (S . t) & (F Toler ) .: (A /\ (S . t)) c= R )
A5: ( S . t is open & t in S . t ) by A2;
(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 A6: FSh in (F Toler ) .: (A /\ (S . t)) ; :: thesis: FSh in R
consider h being set such that
A7: ( h in dom (F Toler ) & h in A /\ (S . t) & FSh = (F Toler ) . h ) by A6, FUNCT_1:def 12;
reconsider h' = h as Point of T by A7;
( h' in S . t & h' in A & FSh = (F . h') . h' ) by A7, Def8, XBOOLE_0:def 4;
then A8: ( h' in A & FSh = Ft . h' ) by A2;
the carrier of T = dom Ft by FUNCT_2:def 1;
then FSh in Ft .: A by A8, FUNCT_1:def 12;
hence FSh in R by A4; :: thesis: verum

end;

hence ( A /\ (S . t) is open & t in A /\ (S . t) & (F Toler ) .: (A /\ (S . t)) c= R ) by A4, A5, TOPS_1:38, 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