for p being Point of X
for V being Subset of COMPLEX st (a (#) f) . p in V & V is open holds
ex W being Subset of X st
( p in W & W is open & (a (#) f) .: W c= V )

let p be Point of X; :: thesis:
let V be Subset of COMPLEX; :: thesis:
assume A3: ( (a (#) f) . p in V & V is open ) ; :: thesis:
reconsider z0 = (a (#) f) . p as Complex ;
consider N being Neighbourhood of z0 such that
A4: N c= V by A3, CFDIFF_1:9;
consider r being Real such that
A5: ( 0 < r & { y where y is Complex : |.(y - z0).| < r } c= N ) by CFDIFF_1:def 5;
set S = { y where y is Complex : |.(y - z0).| < r } ;
A6: |.a.| > 0 by A2;
A7: r / |.a.| > 0 by A2, A5;
reconsider z1 = f . p as Complex ;
set S1 = { y where y is Complex : |.(y - z1).| < r / |.a.| } ;
{ y where y is Complex : |.(y - z1).| < r / |.a.| } c= COMPLEX

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

end;

then reconsider T1 = { y where y is Complex : |.(y - z1).| < r / |.a.| } as Subset of COMPLEX ;
A8: T1 is open by CFDIFF_1:13;
|.(z1 - z1).| = 0 ;
then z1 in { y where y is Complex : |.(y - z1).| < r / |.a.| } by A7;
then consider W1 being Subset of X such that
A9: ( p in W1 & W1 is open & f .: W1 c= { y where y is Complex : |.(y - z1).| < r / |.a.| } ) by A8, Th3;
set W = W1;
A10: W1 is open by A9;
A11: p in W1 by A9;
(a (#) f) .: W1 c= { y where y is Complex : |.(y - z0).| < r }

let z3 be object ; :: according to TARSKI:def 3 :: thesis:
assume z3 in (a (#) f) .: W1 ; :: thesis:
then consider x3 being object such that
A12: ( x3 in dom (a (#) f) & x3 in W1 & (a (#) f) . x3 = z3 ) by FUNCT_1:def 6;
reconsider px = x3 as Point of X by A12;
px in the carrier of X ;
then px in dom f by FUNCT_2:def 1;
then f . px in f .: W1 by A12, FUNCT_1:def 6;
then A13: f . px in { y where y is Complex : |.(y - z1).| < r / |.a.| } by A9;
reconsider a1 = f . px as Complex ;
ex aa1 being Complex st
( f . px = aa1 & |.(aa1 - z1).| < r / |.a.| ) by A13;
then A14: |.(a1 - z1).| < r / |.a.| ;
A15: |.(((a (#) f) . x3) - z0).| = |.((a * (f . px)) - z0).| by A1
.= |.((a * (f . px)) - (a * (f . p))).| by A1
.= |.(a * ((f . px) - (f . p))).|
.= |.a.| * |.(a1 - z1).| by COMPLEX1:65 ;
A16: |.a.| * |.(a1 - z1).| < |.a.| * (r / |.a.|) by A6, A14, XREAL_1:68;
|.a.| * (r / |.a.|) = r * (|.a.| / |.a.|)
.= r * 1 by A6, XCMPLX_1:60
.= r ;
then |.(((a (#) f) . px) - z0).| < r by A15, A16;
hence z3 in { y where y is Complex : |.(y - z0).| < r } by A12; :: thesis:

end;

then (a (#) f) .: W1 c= N by A5;
hence ex W being Subset of X st
( p in W & W is open & (a (#) f) .: W c= V ) by A10, A11, A4, XBOOLE_1:1; :: thesis:

end;

end;

set g = X --> 0c;
set CX = the carrier of X;
A18: dom (X --> 0c) = the carrier of X by FUNCOP_1:13;
dom (a (#) f) = the carrier of X by FUNCT_2:def 1;
then A19: dom (X --> 0c) = dom (a (#) f) by A18;
for z being object st z in dom (a (#) f) holds
(X --> 0c) . z = (a (#) f) . z

let z be object ; :: thesis:
assume A20: z in dom (a (#) f) ; :: thesis:
(a (#) f) . z = 0 * (f . z) by A17, VALUED_1:6
.= 0 ;
hence (X --> 0c) . z = (a (#) f) . z by A20, FUNCOP_1:7; :: thesis:

end;

end;