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 A2: ( 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 number such that
A3: ( 0 < r & ].(r0 - r),(r0 + r).[ c= V ) by A2, 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 set ; :: 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 ; :: thesis: verum

end;

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

proof

let x be set ; :: 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 set such that
A8: ( z in dom h & z in W1 & h . z = x ) by FUNCT_1:def 6;
A9: z in W1 by A8;
reconsider pz = z as Point of X by A8;
pz in the carrier of X ;
then pz in dom f by FUNCT_2:def 1;
then f . pz in f .: W1 by A9, FUNCT_1:def 6;
then A10: f . pz in { y where y is Complex : |.(y - z1).| < r } by A5;
reconsider a1 = f . pz as Complex ;
ex aa1 being Complex st
( f . pz = aa1 & |.(aa1 - z1).| < r ) by A10;
then A11: |.(a1 - z1).| < r ;
A12: |.((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 A11, XXREAL_0:2;
hence x in ].(r0 - r),(r0 + r).[ by A8, RCOMP_1:1, A12; :: thesis: verum

end;

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

end;

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