let T be non empty TopSpace; :: thesis: for F, G being RealMap of T st F is continuous & G is continuous holds
F + G is continuous
let F, G be RealMap of T; :: thesis: ( F is continuous & G is continuous implies F + G is continuous )
assume A1: ( F is continuous & G is continuous ) ; :: thesis: F + G is continuous
reconsider F' = F, G' = G, FG' = F + G as Function of T,R^1 by TOPMETR:24;
A2: ( F' is continuous & G' is continuous ) by A1, TOPREAL6:83;

now

let t be Point of T; :: thesis: FG' is_continuous_at t
for R being Subset of R^1 st R is open & FG' . t in R holds
ex H being Subset of T st
( H is open & t in H & FG' .: H c= R )

proof

let R be Subset of R^1 ; :: thesis: ( R is open & FG' . t in R implies ex H being Subset of T st
( H is open & t in H & FG' .: H c= R ) )
assume A3: ( R is open & FG' . t in R ) ; :: thesis: ex H being Subset of T st
( H is open & t in H & FG' .: H c= R )
reconsider Ft = F . t, Gt = G . t, FGt = (F + G) . t as Point of RealSpace by METRIC_1:def 14;
consider r being real number such that
A4: ( r > 0 & Ball FGt,r c= R ) by A3, TOPMETR:22, TOPMETR:def 7;
reconsider r' = r as Real by XREAL_0:def 1;
A5: r' / 2 > 0 by A4, XREAL_1:141;
reconsider A = Ball Ft,(r' / 2), B = Ball Gt,(r' / 2) as Subset of R^1 by METRIC_1:def 14, TOPMETR:24;
A6: ( F' . t in A & A is open & G . t in B & B is open ) by A5, Lm7, TOPMETR:21, TOPMETR:def 7;
F' is_continuous_at t by A2, TMAP_1:55;
then consider AT being Subset of T such that
A7: ( AT is open & t in AT & F' .: AT c= A ) by A6, TMAP_1:48;
G' is_continuous_at t by A2, TMAP_1:55;
then consider BT being Subset of T such that
A8: ( BT is open & t in BT & G' .: BT c= B ) by A6, TMAP_1:48;
A9: ( AT /\ BT is open & t in AT /\ BT ) by A7, A8, TOPS_1:38, XBOOLE_0:def 4;
(F + G) .: (AT /\ BT) c= R

proof

let FGx be set ; :: according to TARSKI:def 3 :: thesis: ( not FGx in (F + G) .: (AT /\ BT) or FGx in R )
assume FGx in (F + G) .: (AT /\ BT) ; :: thesis: FGx in R
then consider x being set such that
A10: ( x in dom (F + G) & x in AT /\ BT & FGx = (F + G) . x ) by FUNCT_1:def 12;
reconsider x = x as Point of T by A10;
reconsider Fx = F . x, Gx = G . x, FGx' = (F + G) . x as Point of RealSpace by METRIC_1:def 14;
( dom F = the carrier of T & dom G = the carrier of T ) by FUNCT_2:def 1;
then ( x in dom F & x in AT & x in dom G & x in BT ) by A10, XBOOLE_0:def 4;
then ( F . x in F .: AT & G . x in G .: BT ) by FUNCT_1:def 12;
then ( dist Fx,Ft < r' / 2 & dist Gx,Gt < r' / 2 ) by A7, A8, METRIC_1:12;
then ( abs ((F . x) - (F . t)) < r' / 2 & abs ((G . x) - (G . t)) < r' / 2 ) by TOPMETR:15;
then ( - (r' / 2) < (F . x) - (F . t) & - (r' / 2) < (G . x) - (G . t) & (F . x) - (F . t) < r' / 2 & (G . x) - (G . t) < r' / 2 ) by SEQ_2:9;
then ( (- (r' / 2)) + (- (r' / 2)) < ((F . x) - (F . t)) + ((G . x) - (G . t)) & ((F . x) - (F . t)) + ((G . x) - (G . t)) < (r' / 2) + (r' / 2) ) by XREAL_1:10;
then ( - r' < ((F . x) + (G . x)) - ((F . t) + (G . t)) & ((F . x) + (G . x)) - ((F . t) + (G . t)) < r' ) ;
then abs (((F . x) + (G . x)) - ((F . t) + (G . t))) < r' by SEQ_2:9;
then abs (((F + G) . x) - ((F . t) + (G . t))) < r' by Def7;
then abs (((F + G) . x) - ((F + G) . t)) < r' by Def7;
then dist FGt,FGx' < r' by TOPMETR:15;
then FGx' in Ball FGt,r by METRIC_1:12;
hence FGx in R by A4, A10; :: thesis: verum

end;

hence ex H being Subset of T st
( H is open & t in H & FG' .: H c= R ) by A9; :: thesis: verum

end;

hence FG' is_continuous_at t by TMAP_1:48; :: thesis: verum

end;

then FG' is continuous by TMAP_1:55;
hence F + G is continuous by TOPREAL6:83; :: thesis: verum