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 that
A1: F is continuous and
A2: G is continuous ; :: thesis: F + G is continuous
reconsider F9 = F, G9 = G, FG9 = F + G as Function of T,R^1 by TOPMETR:17;
A3: G9 is continuous by A2, JORDAN5A:27;
A4: F9 is continuous by A1, JORDAN5A:27;

now :: thesis: for t being Point of T holds FG9 is_continuous_at t

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

proof

reconsider Ft = F . t, Gt = G . t, FGt = (F + G) . t as Point of RealSpace by METRIC_1:def 13;
let R be Subset of R^1; :: thesis: ( R is open & FG9 . t in R implies ex H being Subset of T st
( H is open & t in H & FG9 .: H c= R ) )
assume ( R is open & FG9 . t in R ) ; :: thesis: ex H being Subset of T st
( H is open & t in H & FG9 .: H c= R )
then consider r being Real such that
A5: r > 0 and
A6: Ball (FGt,r) c= R by TOPMETR:15, TOPMETR:def 6;
reconsider r9 = r as Real ;
reconsider A = Ball (Ft,(r9 / 2)), B = Ball (Gt,(r9 / 2)) as Subset of R^1 by METRIC_1:def 13, TOPMETR:17;
A7: ( A is open & F9 is_continuous_at t ) by A4, TMAP_1:50, TOPMETR:14, TOPMETR:def 6;
F9 . t in A by A5, Lm7, XREAL_1:139;
then consider AT being Subset of T such that
A8: AT is open and
A9: t in AT and
A10: F9 .: AT c= A by A7, TMAP_1:43;
A11: ( B is open & G9 is_continuous_at t ) by A3, TMAP_1:50, TOPMETR:14, TOPMETR:def 6;
G . t in B by A5, Lm7, XREAL_1:139;
then consider BT being Subset of T such that
A12: BT is open and
A13: t in BT and
A14: G9 .: BT c= B by A11, TMAP_1:43;
A15: (F + G) .: (AT /\ BT) c= R

proof

let FGx be object ; :: 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 object such that
A16: x in dom (F + G) and
A17: x in AT /\ BT and
A18: FGx = (F + G) . x by FUNCT_1:def 6;
reconsider x = x as Point of T by A16;
reconsider Fx = F . x, Gx = G . x, FGx9 = (F + G) . x as Point of RealSpace by METRIC_1:def 13;
( dom G = the carrier of T & x in BT ) by A17, FUNCT_2:def 1, XBOOLE_0:def 4;
then G . x in G .: BT by FUNCT_1:def 6;
then dist (Gx,Gt) < r9 / 2 by A14, METRIC_1:11;
then A19: |.((G . x) - (G . t)).| < r9 / 2 by TOPMETR:11;
then A20: - (r9 / 2) < (G . x) - (G . t) by SEQ_2:1;
( dom F = the carrier of T & x in AT ) by A17, FUNCT_2:def 1, XBOOLE_0:def 4;
then F . x in F .: AT by FUNCT_1:def 6;
then dist (Fx,Ft) < r9 / 2 by A10, METRIC_1:11;
then A21: |.((F . x) - (F . t)).| < r9 / 2 by TOPMETR:11;
then - (r9 / 2) < (F . x) - (F . t) by SEQ_2:1;
then (- (r9 / 2)) + (- (r9 / 2)) < ((F . x) - (F . t)) + ((G . x) - (G . t)) by A20, XREAL_1:8;
then A22: - r9 < ((F . x) + (G . x)) - ((F . t) + (G . t)) ;
A23: (G . x) - (G . t) < r9 / 2 by A19, SEQ_2:1;
(F . x) - (F . t) < r9 / 2 by A21, SEQ_2:1;
then ((F . x) - (F . t)) + ((G . x) - (G . t)) < (r9 / 2) + (r9 / 2) by A23, XREAL_1:8;
then |.(((F . x) + (G . x)) - ((F . t) + (G . t))).| < r9 by A22, SEQ_2:1;
then |.(((F + G) . x) - ((F . t) + (G . t))).| < r9 by Def7;
then |.(((F + G) . x) - ((F + G) . t)).| < r9 by Def7;
then dist (FGt,FGx9) < r9 by TOPMETR:11;
then FGx9 in Ball (FGt,r) by METRIC_1:11;
hence FGx in R by A6, A18; :: thesis: verum

end;

t in AT /\ BT by A9, A13, XBOOLE_0:def 4;
hence ex H being Subset of T st
( H is open & t in H & FG9 .: H c= R ) by A8, A12, A15; :: thesis: verum

end;

hence FG9 is_continuous_at t by TMAP_1:43; :: thesis: verum

end;

then FG9 is continuous by TMAP_1:50;
hence F + G is continuous by JORDAN5A:27; :: thesis: verum