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 by MEMBERED:1;
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 } ;
A6: r / 2 is Real by XREAL_0:def 1;
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 set ; :: 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 ;
A7: T1 is open by A6, 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
A8: ( p in W1 & W1 is open & f .: W1 c= { y where y is Complex : |.(y - z1).| < r / 2 } ) by A7, 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 set ; :: 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 ;
A9: T2 is open by A6, 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
A10: ( p in W2 & W2 is open & g .: W2 c= { y where y is Complex : |.(y - z2).| < r / 2 } ) by A9, Th3;
set W = W1 /\ W2;
A11: W1 /\ W2 is open by A8, A10, TOPS_1:11;
A12: p in W1 /\ W2 by A8, A10, XBOOLE_0:def 4;
h .: (W1 /\ W2) c= { y where y is Complex : |.(y - z0).| < r }

proof

let z3 be set ; :: 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 set such that
A13: ( x3 in dom h & x3 in W1 /\ W2 & h . x3 = z3 ) by FUNCT_1:def 6;
A14: x3 in W1 by A13, XBOOLE_0:def 4;
reconsider px = x3 as Point of X by A13;
A15: px in the carrier of X ;
then px in dom f by FUNCT_2:def 1;
then f . px in f .: W1 by A14, FUNCT_1:def 6;
then A16: f . px in { y where y is Complex : |.(y - z1).| < r / 2 } by A8;
reconsider a1 = f . px as Complex ;
A17: ex aa1 being Complex st
( f . px = aa1 & |.(aa1 - z1).| < r / 2 ) by A16;
A18: x3 in W2 by A13, XBOOLE_0:def 4;
px in dom g by A15, FUNCT_2:def 1;
then g . px in g .: W2 by A18, FUNCT_1:def 6;
then A19: g . px in { y where y is Complex : |.(y - z2).| < r / 2 } by A10;
reconsider a2 = g . px as Complex ;
ex aa2 being Complex st
( g . px = aa2 & |.(aa2 - z2).| < r / 2 ) by A19;
then A20: |.(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 A21: |.((h . px) - z0).| <= |.(a1 - z1).| + |.(a2 - z2).| by COMPLEX1:56;
A22: |.(a1 - z1).| + |.(a2 - z2).| < (r / 2) + |.(a2 - z2).| by A17, XREAL_1:8;
(r / 2) + |.(a2 - z2).| < (r / 2) + (r / 2) by A20, XREAL_1:8;
then |.(a1 - z1).| + |.(a2 - z2).| < r by A22, XXREAL_0:2;
then |.((h . px) - z0).| < r by A21, XXREAL_0:2;
hence z3 in { y where y is Complex : |.(y - z0).| < r } by A13; :: thesis: verum

end;

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

end;

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