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;

hence F + G is continuous by JORDAN5A:27; :: thesis: verum

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

then
FG9 is continuous
by TMAP_1:50;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 )

end;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

hence
FG9 is_continuous_at t
by TMAP_1:43; :: thesis: verum
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

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;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

t in AT /\ BT
by A9, A13, XBOOLE_0:def 4;
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;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

hence ex H being Subset of T st

( H is open & t in H & FG9 .: H c= R ) by A8, A12, A15; :: thesis: verum

hence F + G is continuous by JORDAN5A:27; :: thesis: verum