let X be non empty TopSpace; :: thesis: for f, g being continuous Function of the carrier of X,COMPLEX holds f + g is continuous Function of the carrier of X,COMPLEX
let f, g be continuous Function of the carrier of X,COMPLEX; :: thesis: f + g is continuous Function of the carrier of X,COMPLEX
set h = f + g;
A1: rng (f + g) c= COMPLEX ;
dom (f + g) = (dom f) /\ (dom g) by VALUED_1:def 1
.= the carrier of X /\ (dom g) by PARTFUN1:def 2
.= the carrier of X /\ the carrier of X by PARTFUN1:def 2 ;
then reconsider h = f + g as Function of the carrier of X,COMPLEX by A1, FUNCT_2:2;
A2: for x being Point of X holds h . x = (f . x) + (g . x) by VALUED_1:1;
for p being Point of X
for V being Subset of COMPLEX 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 COMPLEX 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 COMPLEX; :: 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 A3: ( 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 z0 = h . 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 } ;
reconsider z1 = f . p as Complex ;
set S1 = { y where y is Complex : |.(y - z1).| < r / 2 } ;
{ y where y is Complex : |.(y - z1).| < r / 2 } c= COMPLEX

proof

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

end;

then reconsider T1 = { y where y is Complex : |.(y - z1).| < r / 2 } as Subset of COMPLEX ;
A6: T1 is open by CFDIFF_1:13;
|.(z1 - z1).| = 0 ;
then z1 in { y where y is Complex : |.(y - z1).| < r / 2 } by A5;
then consider W1 being Subset of X such that
A7: ( p in W1 & W1 is open & f .: W1 c= { y where y is Complex : |.(y - z1).| < r / 2 } ) by A6, Th3;
reconsider z2 = g . p as Complex ;
set S2 = { y where y is Complex : |.(y - z2).| < r / 2 } ;
{ y where y is Complex : |.(y - z2).| < r / 2 } c= COMPLEX

proof

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

end;

then reconsider T2 = { y where y is Complex : |.(y - z2).| < r / 2 } as Subset of COMPLEX ;
A8: T2 is open by CFDIFF_1:13;
|.(z2 - z2).| = 0 ;
then z2 in { y where y is Complex : |.(y - z2).| < r / 2 } by A5;
then consider W2 being Subset of X such that
A9: ( p in W2 & W2 is open & g .: W2 c= { y where y is Complex : |.(y - z2).| < r / 2 } ) by A8, Th3;
set W = W1 /\ W2;
A10: W1 /\ W2 is open by A7, A9, TOPS_1:11;
A11: p in W1 /\ W2 by A7, A9, XBOOLE_0:def 4;
h .: (W1 /\ W2) c= { y where y is Complex : |.(y - z0).| < r }

proof

let z3 be object ; :: according to TARSKI:def 3 :: thesis: ( not z3 in h .: (W1 /\ W2) or z3 in { y where y is Complex : |.(y - z0).| < r } )
assume z3 in h .: (W1 /\ W2) ; :: thesis: z3 in { y where y is Complex : |.(y - z0).| < r }
then consider x3 being object such that
A12: ( x3 in dom h & x3 in W1 /\ W2 & h . x3 = z3 ) by FUNCT_1:def 6;
A13: x3 in W1 by A12, XBOOLE_0:def 4;
reconsider px = x3 as Point of X by A12;
A14: px in the carrier of X ;
then px in dom f by FUNCT_2:def 1;
then f . px in f .: W1 by A13, FUNCT_1:def 6;
then A15: f . px in { y where y is Complex : |.(y - z1).| < r / 2 } by A7;
reconsider a1 = f . px as Complex ;
A16: ex aa1 being Complex st
( f . px = aa1 & |.(aa1 - z1).| < r / 2 ) by A15;
A17: x3 in W2 by A12, XBOOLE_0:def 4;
px in dom g by A14, FUNCT_2:def 1;
then g . px in g .: W2 by A17, FUNCT_1:def 6;
then A18: g . px in { y where y is Complex : |.(y - z2).| < r / 2 } by A9;
reconsider a2 = g . px as Complex ;
ex aa2 being Complex st
( g . px = aa2 & |.(aa2 - z2).| < r / 2 ) by A18;
then A19: |.(a2 - z2).| < r / 2 ;
|.((h . x3) - z0).| = |.(((f . px) + (g . px)) - z0).| by A2
.= |.(((f . px) + (g . px)) - ((f . p) + (g . p))).| by A2
.= |.((a1 - z1) + (a2 - z2)).| ;
then A20: |.((h . px) - z0).| <= |.(a1 - z1).| + |.(a2 - z2).| by COMPLEX1:56;
A21: |.(a1 - z1).| + |.(a2 - z2).| < (r / 2) + |.(a2 - z2).| by A16, XREAL_1:8;
(r / 2) + |.(a2 - z2).| < (r / 2) + (r / 2) by A19, XREAL_1:8;
then |.(a1 - z1).| + |.(a2 - z2).| < r by A21, XXREAL_0:2;
then |.((h . px) - z0).| < r by A20, XXREAL_0:2;
hence z3 in { y where y is Complex : |.(y - z0).| < r } by A12; :: thesis: verum

end;

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

end;

hence f + g is continuous Function of the carrier of X,COMPLEX by Th3; :: thesis: verum