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

proof

let p be Point of X; :: thesis: for V being Subset of REAL st h . p in V & V is open holds
ex W being Subset of X st
( p in W & W is open & h .: W c= V )
let V be Subset of REAL; :: thesis: ( h . p in V & V is open implies ex W being Subset of X st
( p in W & W is open & h .: W c= V ) )
assume A1: ( h . p in V & V is open ) ; :: thesis: ex W being Subset of X st
( p in W & W is open & h .: W c= V )
reconsider r0 = h . p as Real ;
consider r being Real such that
A2: ( 0 < r & ].(r0 - r),(r0 + r).[ c= V ) by A1, RCOMP_1:19;
set S = ].(r0 - r),(r0 + r).[;
reconsider z1 = f . p as Complex ;
set S1 = { y where y is Complex : |.(y - z1).| < r } ;
{ y where y is Complex : |.(y - z1).| < r } c= COMPLEX

proof

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

end;

then reconsider T1 = { y where y is Complex : |.(y - z1).| < r } as Subset of COMPLEX ;
A3: T1 is open by CFDIFF_1:13;
|.(z1 - z1).| = 0 ;
then z1 in { y where y is Complex : |.(y - z1).| < r } by A2;
then consider W1 being Subset of X such that
A4: ( p in W1 & W1 is open & f .: W1 c= { y where y is Complex : |.(y - z1).| < r } ) by A3, Th3;
set W = W1;
A5: W1 is open by A4;
A6: p in W1 by A4;
h .: W1 c= ].(r0 - r),(r0 + r).[

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in h .: W1 or x in ].(r0 - r),(r0 + r).[ )
assume x in h .: W1 ; :: thesis: x in ].(r0 - r),(r0 + r).[
then consider z being object such that
A7: ( z in dom h & z in W1 & h . z = x ) by FUNCT_1:def 6;
A8: z in W1 by A7;
reconsider pz = z as Point of X by A7;
pz in the carrier of X ;
then pz in dom f by FUNCT_2:def 1;
then f . pz in f .: W1 by A8, FUNCT_1:def 6;
then A9: f . pz in { y where y is Complex : |.(y - z1).| < r } by A4;
reconsider a1 = f . pz as Complex ;
ex aa1 being Complex st
( f . pz = aa1 & |.(aa1 - z1).| < r ) by A9;
then A10: |.(a1 - z1).| < r ;
A11: |.((h . z) - r0).| = |.(|.(f . pz).| - (|.f.| . p)).| by VALUED_1:18
.= |.(|.(f . pz).| - |.(f . p).|).| by VALUED_1:18 ;
|.(|.(f . pz).| - |.(f . p).|).| <= |.((f . pz) - (f . p)).| by COMPLEX1:64;
then |.(|.(f . pz).| - |.(f . p).|).| < r by A10, XXREAL_0:2;
hence x in ].(r0 - r),(r0 + r).[ by A7, A11, RCOMP_1:1; :: thesis: verum

end;

hence ex W being Subset of X st
( p in W & W is open & h .: W c= V ) by A5, A6, A2, XBOOLE_1:1; :: thesis: verum

end;

hence ( |.f.| is Function of the carrier of X,REAL & |.f.| is continuous ) by C0SP2:1; :: thesis: verum