let x be Point of X; :: thesis:
let V be Subset of COMPLEX; :: thesis:
set z = f . x;
reconsider z0 = f . x as Complex ;
assume ( f . x in V & V is open ) ; :: thesis:
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

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

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:
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:
thus W is open by A1, A4, Th2; :: thesis:
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:

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:

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:

let x be Point of X; :: thesis:
assume x in (f " Y) ` ; :: thesis:
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:
thus W is a_neighborhood of x by A8, CONNSP_2:3; :: thesis:
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:

end;

end;