let c be Real; :: thesis: for f, g being PartFunc of REAL,REAL st f is continuous & g is continuous & f . c = g . c & ].-infty,c.] c= dom f & [.c,+infty.[ c= dom g holds
(f | ].-infty,c.]) +* (g | [.c,+infty.[) is continuous
let f, g be PartFunc of REAL,REAL; :: thesis: ( f is continuous & g is continuous & f . c = g . c & ].-infty,c.] c= dom f & [.c,+infty.[ c= dom g implies (f | ].-infty,c.]) +* (g | [.c,+infty.[) is continuous )
assume that
A1a: ( f is continuous & g is continuous ) and
A2: f . c = g . c and
A3: ( ].-infty,c.] c= dom f & [.c,+infty.[ c= dom g ) ; :: thesis: (f | ].-infty,c.]) +* (g | [.c,+infty.[) is continuous
set F = (f | ].-infty,c.]) +* (g | [.c,+infty.[);
set Df = ].-infty,c.];
set Dg = [.c,+infty.[;
A1: ( f | ].-infty,c.] is continuous & g | [.c,+infty.[ is continuous ) by A1a;
AD: ( dom (f | ].-infty,c.]) = ].-infty,c.] & dom (g | [.c,+infty.[) = [.c,+infty.[ ) by RELAT_1:62, A3;
A7: ( c in ].-infty,c.] & c in [.c,+infty.[ ) by XXREAL_1:234, XXREAL_1:236;
for x0 being Real st x0 in dom ((f | ].-infty,c.]) +* (g | [.c,+infty.[)) holds
(f | ].-infty,c.]) +* (g | [.c,+infty.[) is_continuous_in x0

proof

let x0 be Real; :: thesis: ( x0 in dom ((f | ].-infty,c.]) +* (g | [.c,+infty.[)) implies (f | ].-infty,c.]) +* (g | [.c,+infty.[) is_continuous_in x0 )
assume x0 in dom ((f | ].-infty,c.]) +* (g | [.c,+infty.[)) ; :: thesis: (f | ].-infty,c.]) +* (g | [.c,+infty.[) is_continuous_in x0
for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Real st x1 in dom ((f | ].-infty,c.]) +* (g | [.c,+infty.[)) & |.(x1 - x0).| < s holds
|.((((f | ].-infty,c.]) +* (g | [.c,+infty.[)) . x1) - (((f | ].-infty,c.]) +* (g | [.c,+infty.[)) . x0)).| < r ) )

proof

let r be Real; :: thesis: ( 0 < r implies ex s being Real st
( 0 < s & ( for x1 being Real st x1 in dom ((f | ].-infty,c.]) +* (g | [.c,+infty.[)) & |.(x1 - x0).| < s holds
|.((((f | ].-infty,c.]) +* (g | [.c,+infty.[)) . x1) - (((f | ].-infty,c.]) +* (g | [.c,+infty.[)) . x0)).| < r ) ) )
assume A4: 0 < r ; :: thesis: ex s being Real st
( 0 < s & ( for x1 being Real st x1 in dom ((f | ].-infty,c.]) +* (g | [.c,+infty.[)) & |.(x1 - x0).| < s holds
|.((((f | ].-infty,c.]) +* (g | [.c,+infty.[)) . x1) - (((f | ].-infty,c.]) +* (g | [.c,+infty.[)) . x0)).| < r ) )

per cases ( x0 < c or x0 >= c ) ;

suppose P2a: x0 < c ; :: thesis: ex s being Real st
( 0 < s & ( for x1 being Real st x1 in dom ((f | ].-infty,c.]) +* (g | [.c,+infty.[)) & |.(x1 - x0).| < s holds
|.((((f | ].-infty,c.]) +* (g | [.c,+infty.[)) . x1) - (((f | ].-infty,c.]) +* (g | [.c,+infty.[)) . x0)).| < r ) )

then P2: x0 in ].-infty,c.] by XXREAL_1:234;
consider sf being Real such that
P3: 0 < sf and
P4: for x1 being Real st x1 in ].-infty,c.] & |.(x1 - x0).| < sf holds
|.((f . x1) - (f . x0)).| < r / 2 by FCONT_1:14, A1, A3, P2, A4;
consider sg being Real such that
P8: 0 < sg and
P9: for x1 being Real st x1 in [.c,+infty.[ & |.(x1 - c).| < sg holds
|.((g . x1) - (g . c)).| < r / 2 by FCONT_1:14, A1, A3, A7, A4;
SMin: ( min (sf,sg) <= sf & min (sf,sg) <= sg ) by XXREAL_0:17;
take min (sf,sg) ; :: thesis: ( 0 < min (sf,sg) & ( for x1 being Real st x1 in dom ((f | ].-infty,c.]) +* (g | [.c,+infty.[)) & |.(x1 - x0).| < min (sf,sg) holds
|.((((f | ].-infty,c.]) +* (g | [.c,+infty.[)) . x1) - (((f | ].-infty,c.]) +* (g | [.c,+infty.[)) . x0)).| < r ) )
for x1 being Real st x1 in dom ((f | ].-infty,c.]) +* (g | [.c,+infty.[)) & |.(x1 - x0).| < min (sf,sg) holds
|.((((f | ].-infty,c.]) +* (g | [.c,+infty.[)) . x1) - (((f | ].-infty,c.]) +* (g | [.c,+infty.[)) . x0)).| < r

proof

let x1 be Real; :: thesis: ( x1 in dom ((f | ].-infty,c.]) +* (g | [.c,+infty.[)) & |.(x1 - x0).| < min (sf,sg) implies |.((((f | ].-infty,c.]) +* (g | [.c,+infty.[)) . x1) - (((f | ].-infty,c.]) +* (g | [.c,+infty.[)) . x0)).| < r )
assume that
x1 in dom ((f | ].-infty,c.]) +* (g | [.c,+infty.[)) and
P7: |.(x1 - x0).| < min (sf,sg) ; :: thesis: |.((((f | ].-infty,c.]) +* (g | [.c,+infty.[)) . x1) - (((f | ].-infty,c.]) +* (g | [.c,+infty.[)) . x0)).| < r
PF: |.((((f | ].-infty,c.]) +* (g | [.c,+infty.[)) . x1) - (((f | ].-infty,c.]) +* (g | [.c,+infty.[)) . x0)).| = |.((((f | ].-infty,c.]) +* (g | [.c,+infty.[)) . x1) - ((f | ].-infty,c.]) . x0)).| by FUNCT_4:11, XXREAL_1:236, P2a, AD
.= |.((((f | ].-infty,c.]) +* (g | [.c,+infty.[)) . x1) - (f . x0)).| by FUNCT_1:49, XXREAL_1:234, P2a ;

per cases ( x1 < c or x1 >= c ) ;

suppose P11: x1 < c ; :: thesis: |.((((f | ].-infty,c.]) +* (g | [.c,+infty.[)) . x1) - (((f | ].-infty,c.]) +* (g | [.c,+infty.[)) . x0)).| < r

then not x1 in [.c,+infty.[ by XXREAL_1:236;
then P12: not x1 in dom (g | [.c,+infty.[) by RELAT_1:62, A3;
P13: x1 in ].-infty,c.] by XXREAL_1:234, P11;
P7a: |.(x1 - x0).| < sf by XXREAL_0:2, P7, SMin;
|.((((f | ].-infty,c.]) +* (g | [.c,+infty.[)) . x1) - (((f | ].-infty,c.]) +* (g | [.c,+infty.[)) . x0)).| = |.(((f | ].-infty,c.]) . x1) - (f . x0)).| by FUNCT_4:11, P12, PF
.= |.((f . x1) - (f . x0)).| by FUNCT_1:49, XXREAL_1:234, P11 ;
then P14: |.((((f | ].-infty,c.]) +* (g | [.c,+infty.[)) . x1) - (((f | ].-infty,c.]) +* (g | [.c,+infty.[)) . x0)).| < r / 2 by P4, P13, P7a;
(r / 2) + 0 < (r / 2) + (r / 2) by XREAL_1:8, A4;
hence |.((((f | ].-infty,c.]) +* (g | [.c,+infty.[)) . x1) - (((f | ].-infty,c.]) +* (g | [.c,+infty.[)) . x0)).| < r by XXREAL_0:2, P14; :: thesis: verum

end;

suppose P21: x1 >= c ; :: thesis: |.((((f | ].-infty,c.]) +* (g | [.c,+infty.[)) . x1) - (((f | ].-infty,c.]) +* (g | [.c,+infty.[)) . x0)).| < r

then P22: x1 in [.c,+infty.[ by XXREAL_1:236;
P22b: x0 <= x1 by P2a, P21, XXREAL_0:2;
then ( c - c <= x1 - c & x0 - x0 <= x1 - x0 ) by XREAL_1:13, P21;
then X1: ( |.(x1 - c).| = x1 - c & x1 - x0 = |.(x1 - x0).| ) by COMPLEX1:43;
|.(x1 - c).| <= |.(x1 - x0).| by XREAL_1:13, P2a, X1;
then |.(x1 - c).| < min (sf,sg) by XXREAL_0:2, P7;
then |.(x1 - c).| < sg by XXREAL_0:2, SMin;
then P23: |.((g . x1) - (g . c)).| < r / 2 by P9, P22;
c - x0 >= c - c by XREAL_1:13, P2a;
then X2: c - x0 = |.(c - x0).| by COMPLEX1:43;
x0 - x0 <= x1 - x0 by XREAL_1:13, P22b;
then X3: x1 - x0 = |.(x1 - x0).| by COMPLEX1:43;
|.(c - x0).| <= |.(x1 - x0).| by XREAL_1:13, P21, X2, X3;
then |.(c - x0).| < min (sf,sg) by XXREAL_0:2, P7;
then |.(c - x0).| < sf by XXREAL_0:2, SMin;
then P24: |.((f . c) - (f . x0)).| < r / 2 by P4, A7;
x1 in dom (g | [.c,+infty.[) by RELAT_1:62, A3, P22;
then P26: |.((((f | ].-infty,c.]) +* (g | [.c,+infty.[)) . x1) - (((f | ].-infty,c.]) +* (g | [.c,+infty.[)) . x0)).| = |.(((g | [.c,+infty.[) . x1) - (f . x0)).| by FUNCT_4:13, PF
.= |.((((g . x1) - (g . c)) + (f . c)) - (f . x0)).| by A2, FUNCT_1:49, XXREAL_1:236, P21 ;
P27: |.(((g . x1) - (g . c)) + ((f . c) - (f . x0))).| <= |.((g . x1) - (g . c)).| + |.((f . c) - (f . x0)).| by COMPLEX1:56;
|.((g . x1) - (g . c)).| + |.((f . c) - (f . x0)).| < (r / 2) + (r / 2) by P23, P24, XREAL_1:8;
hence |.((((f | ].-infty,c.]) +* (g | [.c,+infty.[)) . x1) - (((f | ].-infty,c.]) +* (g | [.c,+infty.[)) . x0)).| < r by P26, P27, XXREAL_0:2; :: thesis: verum

end;

end;

end;

hence ( 0 < min (sf,sg) & ( for x1 being Real st x1 in dom ((f | ].-infty,c.]) +* (g | [.c,+infty.[)) & |.(x1 - x0).| < min (sf,sg) holds
|.((((f | ].-infty,c.]) +* (g | [.c,+infty.[)) . x1) - (((f | ].-infty,c.]) +* (g | [.c,+infty.[)) . x0)).| < r ) ) by P3, P8, XXREAL_0:21; :: thesis: verum

end;

suppose Q2a: x0 >= c ; :: thesis: ex s being Real st
( 0 < s & ( for x1 being Real st x1 in dom ((f | ].-infty,c.]) +* (g | [.c,+infty.[)) & |.(x1 - x0).| < s holds
|.((((f | ].-infty,c.]) +* (g | [.c,+infty.[)) . x1) - (((f | ].-infty,c.]) +* (g | [.c,+infty.[)) . x0)).| < r ) )

then Q2: x0 in [.c,+infty.[ by XXREAL_1:236;
Q1: x0 in dom (g | [.c,+infty.[) by RELAT_1:62, A3, Q2;
consider sf being Real such that
Q3: 0 < sf and
Q4: for x1 being Real st x1 in ].-infty,c.] & |.(x1 - c).| < sf holds
|.((f . x1) - (f . c)).| < r / 2 by FCONT_1:14, A1, A3, A7, A4;
consider sg being Real such that
Q8: 0 < sg and
Q9: for x1 being Real st x1 in [.c,+infty.[ & |.(x1 - x0).| < sg holds
|.((g . x1) - (g . x0)).| < r / 2 by FCONT_1:14, A1, A3, A4, Q2;
SMin: ( min (sf,sg) <= sf & min (sf,sg) <= sg ) by XXREAL_0:17;
take min (sf,sg) ; :: thesis: ( 0 < min (sf,sg) & ( for x1 being Real st x1 in dom ((f | ].-infty,c.]) +* (g | [.c,+infty.[)) & |.(x1 - x0).| < min (sf,sg) holds
|.((((f | ].-infty,c.]) +* (g | [.c,+infty.[)) . x1) - (((f | ].-infty,c.]) +* (g | [.c,+infty.[)) . x0)).| < r ) )
for x1 being Real st x1 in dom ((f | ].-infty,c.]) +* (g | [.c,+infty.[)) & |.(x1 - x0).| < min (sf,sg) holds
|.((((f | ].-infty,c.]) +* (g | [.c,+infty.[)) . x1) - (((f | ].-infty,c.]) +* (g | [.c,+infty.[)) . x0)).| < r

proof

let x1 be Real; :: thesis: ( x1 in dom ((f | ].-infty,c.]) +* (g | [.c,+infty.[)) & |.(x1 - x0).| < min (sf,sg) implies |.((((f | ].-infty,c.]) +* (g | [.c,+infty.[)) . x1) - (((f | ].-infty,c.]) +* (g | [.c,+infty.[)) . x0)).| < r )
assume that
x1 in dom ((f | ].-infty,c.]) +* (g | [.c,+infty.[)) and
Q7: |.(x1 - x0).| < min (sf,sg) ; :: thesis: |.((((f | ].-infty,c.]) +* (g | [.c,+infty.[)) . x1) - (((f | ].-infty,c.]) +* (g | [.c,+infty.[)) . x0)).| < r
QF: |.((((f | ].-infty,c.]) +* (g | [.c,+infty.[)) . x1) - (((f | ].-infty,c.]) +* (g | [.c,+infty.[)) . x0)).| = |.((((f | ].-infty,c.]) +* (g | [.c,+infty.[)) . x1) - ((g | [.c,+infty.[) . x0)).| by FUNCT_4:13, Q1
.= |.((((f | ].-infty,c.]) +* (g | [.c,+infty.[)) . x1) - (g . x0)).| by FUNCT_1:49, XXREAL_1:236, Q2a ;

per cases ( x1 < c or x1 >= c ) ;

suppose Q11: x1 < c ; :: thesis: |.((((f | ].-infty,c.]) +* (g | [.c,+infty.[)) . x1) - (((f | ].-infty,c.]) +* (g | [.c,+infty.[)) . x0)).| < r

then Q12: x1 in ].-infty,c.] by XXREAL_1:234;
Q12b: x1 <= x0 by Q2a, XXREAL_0:2, Q11;
then ( c - c <= c - x1 & x0 - x0 <= x0 - x1 ) by XREAL_1:13, Q11;
then X1: ( |.(c - x1).| = c - x1 & x0 - x1 = |.(x0 - x1).| ) by COMPLEX1:43;
|.(c - x1).| <= |.(x0 - x1).| by X1, XREAL_1:13, Q2a;
then |.(- (c - x1)).| <= |.(x0 - x1).| by COMPLEX1:52;
then |.(x1 - c).| <= |.(- (x0 - x1)).| by COMPLEX1:52;
then |.(x1 - c).| < min (sf,sg) by XXREAL_0:2, Q7;
then |.(x1 - c).| < sf by XXREAL_0:2, SMin;
then Q13: |.((f . x1) - (f . c)).| < r / 2 by Q4, Q12;
x0 - c >= c - c by XREAL_1:13, Q2a;
then X2: x0 - c = |.(x0 - c).| by COMPLEX1:43
.= |.(- (x0 - c)).| by COMPLEX1:52 ;
x0 - x0 <= x0 - x1 by XREAL_1:13, Q12b;
then X3: x0 - x1 = |.(x0 - x1).| by COMPLEX1:43
.= |.(- (x0 - x1)).| by COMPLEX1:52 ;
|.(c - x0).| <= |.(x1 - x0).| by XREAL_1:13, X2, X3, Q11;
then |.(c - x0).| < min (sf,sg) by XXREAL_0:2, Q7;
then |.(c - x0).| < sg by XXREAL_0:2, SMin;
then Q14: |.((g . c) - (g . x0)).| < r / 2 by Q9, A7;
Q16: |.((((f | ].-infty,c.]) +* (g | [.c,+infty.[)) . x1) - (((f | ].-infty,c.]) +* (g | [.c,+infty.[)) . x0)).| = |.(((f | ].-infty,c.]) . x1) - (g . x0)).| by FUNCT_4:11, XXREAL_1:236, Q11, AD, QF
.= |.((((f . x1) - (f . c)) + (g . c)) - (g . x0)).| by A2, FUNCT_1:49, Q11, XXREAL_1:234 ;
Q17: |.(((f . x1) - (f . c)) + ((g . c) - (g . x0))).| <= |.((f . x1) - (f . c)).| + |.((g . c) - (g . x0)).| by COMPLEX1:56;
|.((f . x1) - (f . c)).| + |.((g . c) - (g . x0)).| < (r / 2) + (r / 2) by Q13, Q14, XREAL_1:8;
hence |.((((f | ].-infty,c.]) +* (g | [.c,+infty.[)) . x1) - (((f | ].-infty,c.]) +* (g | [.c,+infty.[)) . x0)).| < r by Q16, Q17, XXREAL_0:2; :: thesis: verum

end;

suppose Q21: x1 >= c ; :: thesis: |.((((f | ].-infty,c.]) +* (g | [.c,+infty.[)) . x1) - (((f | ].-infty,c.]) +* (g | [.c,+infty.[)) . x0)).| < r

then Q22: x1 in [.c,+infty.[ by XXREAL_1:236;
Q7a: |.(x1 - x0).| < sg by XXREAL_0:2, Q7, SMin;
|.((((f | ].-infty,c.]) +* (g | [.c,+infty.[)) . x1) - (((f | ].-infty,c.]) +* (g | [.c,+infty.[)) . x0)).| = |.(((g | [.c,+infty.[) . x1) - (g . x0)).| by FUNCT_4:13, XXREAL_1:236, Q21, AD, QF
.= |.((g . x1) - (g . x0)).| by FUNCT_1:49, XXREAL_1:236, Q21 ;
then Q24: |.((((f | ].-infty,c.]) +* (g | [.c,+infty.[)) . x1) - (((f | ].-infty,c.]) +* (g | [.c,+infty.[)) . x0)).| < r / 2 by Q9, Q22, Q7a;
(r / 2) + 0 < (r / 2) + (r / 2) by XREAL_1:8, A4;
hence |.((((f | ].-infty,c.]) +* (g | [.c,+infty.[)) . x1) - (((f | ].-infty,c.]) +* (g | [.c,+infty.[)) . x0)).| < r by XXREAL_0:2, Q24; :: thesis: verum

end;

end;

end;

hence ( 0 < min (sf,sg) & ( for x1 being Real st x1 in dom ((f | ].-infty,c.]) +* (g | [.c,+infty.[)) & |.(x1 - x0).| < min (sf,sg) holds
|.((((f | ].-infty,c.]) +* (g | [.c,+infty.[)) . x1) - (((f | ].-infty,c.]) +* (g | [.c,+infty.[)) . x0)).| < r ) ) by Q3, Q8, XXREAL_0:21; :: thesis: verum

end;

end;

end;

hence (f | ].-infty,c.]) +* (g | [.c,+infty.[) is_continuous_in x0 by FCONT_1:3; :: thesis: verum

end;

hence (f | ].-infty,c.]) +* (g | [.c,+infty.[) is continuous ; :: thesis: verum