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 ;
A4: F9 is continuous by ;
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 ;
reconsider r9 = r as Real ;
reconsider A = Ball (Ft,(r9 / 2)), B = Ball (Gt,(r9 / 2)) as Subset of R^1 by ;
A7: ( A is open & F9 is_continuous_at t ) by ;
F9 . t in A by ;
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 ;
A11: ( B is open & G9 is_continuous_at t ) by ;
G . t in B by ;
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 ;
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 ;
then G . x in G .: BT by FUNCT_1:def 6;
then dist (Gx,Gt) < r9 / 2 by ;
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 ;
then F . x in F .: AT by FUNCT_1:def 6;
then dist (Fx,Ft) < r9 / 2 by ;
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 ;
then A22: - r9 < ((F . x) + (G . x)) - ((F . t) + (G . t)) ;
A23: (G . x) - (G . t) < r9 / 2 by ;
(F . x) - (F . t) < r9 / 2 by ;
then ((F . x) - (F . t)) + ((G . x) - (G . t)) < (r9 / 2) + (r9 / 2) by ;
then |.(((F . x) + (G . x)) - ((F . t) + (G . t))).| < r9 by ;
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 ; :: thesis: verum
end;
t in AT /\ BT by ;
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