let X be non empty TopSpace; :: thesis: for f being Function of the carrier of X,COMPLEX holds
( f is continuous iff for x being Point of X
for V being Subset of COMPLEX st f . x in V & V is open holds
ex W being Subset of X st
( x in W & W is open & f .: W c= V ) )
let f be Function of the carrier of X,COMPLEX; :: thesis: ( f is continuous iff for x being Point of X
for V being Subset of COMPLEX st f . x in V & V is open holds
ex W being Subset of X st
( x in W & W is open & f .: W c= V ) )

hereby :: thesis: ( ( for x being Point of X
for V being Subset of COMPLEX st f . x in V & V is open holds
ex W being Subset of X st
( x in W & W is open & f .: W c= V ) ) implies f is continuous )

assume A1: f is continuous ; :: thesis: for x being Point of X
for V being Subset of COMPLEX st f . x in V & V is open holds
ex W being Subset of X st
( x in W & W is open & f .: W c= V )

now :: thesis: for x being Point of X
for V being Subset of COMPLEX st f . x in V & V is open holds
ex W being Element of bool the carrier of X st
( x in W & W is open & f .: W c= V )

let x be Point of X; :: thesis: for V being Subset of COMPLEX st f . x in V & V is open holds
ex W being Element of bool the carrier of X st
( x in W & W is open & f .: W c= V )
let V be Subset of COMPLEX; :: thesis: ( f . x in V & V is open implies ex W being Element of bool the carrier of X st
( x in W & W is open & f .: W c= V ) )
set z = f . x;
reconsider z0 = f . x as Complex ;
assume ( f . x in V & V is open ) ; :: thesis: ex W being Element of bool the carrier of X st
( x in W & W is open & f .: W c= V )
then consider N being Neighbourhood of z0 such that
A2: N c= V by CFDIFF_1:9;
consider g being Real such that
A3: ( 0 < g & { y where y is Complex : |.(y - z0).| < g } c= N ) by CFDIFF_1:def 5;
set S = { y where y is Complex : |.(y - z0).| < g } ;
{ y where y is Complex : |.(y - z0).| < g } c= COMPLEX

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in { y where y is Complex : |.(y - z0).| < g } or z in COMPLEX )
assume z in { y where y is Complex : |.(y - z0).| < g } ; :: thesis: z in COMPLEX
then ex y being Complex st
( z = y & |.(y - z0).| < g ) ;
hence z in COMPLEX by XCMPLX_0:def 2; :: thesis: verum

end;

then reconsider S1 = { y where y is Complex : |.(y - z0).| < g } as Subset of COMPLEX ;
take W = f " { y where y is Complex : |.(y - z0).| < g } ; :: thesis: ( x in W & W is open & f .: W c= V )
A4: S1 is open by CFDIFF_1:13;
{ y where y is Complex : |.(y - z0).| < g } is Neighbourhood of z0 by A3, CFDIFF_1:6;
then f . x in { y where y is Complex : |.(y - z0).| < g } by CFDIFF_1:7;
hence x in W by FUNCT_2:38; :: thesis: ( W is open & f .: W c= V )
thus W is open by A1, A4, Th2; :: thesis: f .: W c= V
f .: (f " { y where y is Complex : |.(y - z0).| < g } ) c= { y where y is Complex : |.(y - z0).| < g } by FUNCT_1:75;
then f .: W c= N by A3;
hence f .: W c= V by A2; :: thesis: verum

end;

hence for x being Point of X
for V being Subset of COMPLEX st f . x in V & V is open holds
ex W being Subset of X st
( x in W & W is open & f .: W c= V ) ; :: thesis: verum

end;

assume A5: for x being Point of X
for V being Subset of COMPLEX st f . x in V & V is open holds
ex W being Subset of X st
( x in W & W is open & f .: W c= V ) ; :: thesis: f is continuous

now :: thesis: for Y being Subset of COMPLEX st Y is closed holds
f " Y is closed

let Y be Subset of COMPLEX; :: thesis: ( Y is closed implies f " Y is closed )
assume Y is closed ; :: thesis: f " Y is closed
then (Y `) ` is closed ;
then A6: Y ` is open by CFDIFF_1:def 11;
for x being Point of X st x in (f " Y) ` holds
ex W being Subset of X st
( W is a_neighborhood of x & W c= (f " Y) ` )

proof

let x be Point of X; :: thesis: ( x in (f " Y) ` implies ex W being Subset of X st
( W is a_neighborhood of x & W c= (f " Y) ` ) )
assume x in (f " Y) ` ; :: thesis: ex W being Subset of X st
( W is a_neighborhood of x & W c= (f " Y) ` )
then x in f " (Y `) by FUNCT_2:100;
then f . x in Y ` by FUNCT_2:38;
then consider V being Subset of COMPLEX such that
A7: ( f . x in V & V is open & V c= Y ` ) by A6;
consider W being Subset of X such that
A8: ( x in W & W is open & f .: W c= V ) by A5, A7;
take W ; :: thesis: ( W is a_neighborhood of x & W c= (f " Y) ` )
thus W is a_neighborhood of x by A8, CONNSP_2:3; :: thesis: W c= (f " Y) `
f .: W c= Y ` by A7, A8;
then A9: f " (f .: W) c= f " (Y `) by RELAT_1:143;
W c= f " (f .: W) by FUNCT_2:42;
then W c= f " (Y `) by A9;
hence W c= (f " Y) ` by FUNCT_2:100; :: thesis: verum

end;

then (f " Y) ` is open by CONNSP_2:7;
then ((f " Y) `) ` is closed by TOPS_1:4;
hence f " Y is closed ; :: thesis: verum

end;

hence f is continuous ; :: thesis: verum