let f, g be PartFunc of REAL,REAL; :: thesis: ( f is continuous & g is continuous & ex x being object st
( (dom f) /\ (dom g) = {x} & ( for x being object st x in (dom f) /\ (dom g) holds
f . x = g . x ) ) implies ex h being PartFunc of REAL,REAL st
( h = f +* g & ( for x being Real st x in (dom f) /\ (dom g) holds
h is_continuous_in x ) ) )
assume A1: ( f is continuous & g is continuous & ex x being object st
( (dom f) /\ (dom g) = {x} & ( for x being object st x in (dom f) /\ (dom g) holds
f . x = g . x ) ) ) ; :: thesis: ex h being PartFunc of REAL,REAL st
( h = f +* g & ( for x being Real st x in (dom f) /\ (dom g) holds
h is_continuous_in x ) )
reconsider h = f +* g as PartFunc of REAL,REAL ;
take h ; :: thesis: ( h = f +* g & ( for x being Real st x in (dom f) /\ (dom g) holds
h is_continuous_in x ) )
thus h = f +* g ; :: thesis: for x being Real st x in (dom f) /\ (dom g) holds
h is_continuous_in x
let x be Real; :: thesis: ( x in (dom f) /\ (dom g) implies h is_continuous_in x )
J2: h | (dom f) = (g +* f) | (dom f) by FUNCT_4:34, PARTFUN1:def 4, A1
.= f ;
assume x in (dom f) /\ (dom g) ; :: thesis: h is_continuous_in x
then ZR: ( x in dom f & x in dom g ) by XBOOLE_0:def 4;
then JJ: x in dom h by FUNCT_4:12;
for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Real st x1 in dom h & |.(x1 - x).| < s holds
|.((h . x1) - (h . x)).| < 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 h & |.(x1 - x).| < s holds
|.((h . x1) - (h . x)).| < r ) ) )
set hf = h | (dom f);
set hg = h | (dom g);
SF: x in dom (h | (dom f)) by RELAT_1:57, ZR, JJ;
Sf: x in dom (h | (dom g)) by ZR;
assume R0: 0 < r ; :: thesis: ex s being Real st
( 0 < s & ( for x1 being Real st x1 in dom h & |.(x1 - x).| < s holds
|.((h . x1) - (h . x)).| < r ) )
consider s2 being Real such that
SB: ( 0 < s2 & ( for x1 being Real st x1 in dom (h | (dom f)) & |.(x1 - x).| < s2 holds
|.(((h | (dom f)) . x1) - ((h | (dom f)) . x)).| < r / 2 ) ) by J2, ZR, A1, FCONT_1:3, R0;
consider s1 being Real such that
Sb: ( 0 < s1 & ( for x1 being Real st x1 in dom (h | (dom g)) & |.(x1 - x).| < s1 holds
|.(((h | (dom g)) . x1) - ((h | (dom g)) . x)).| < r / 2 ) ) by FCONT_1:3, ZR, A1, R0;
take s = min (s2,s1); :: thesis: ( 0 < s & ( for x1 being Real st x1 in dom h & |.(x1 - x).| < s holds
|.((h . x1) - (h . x)).| < r ) )
thus 0 < s by SB, Sb, XXREAL_0:15; :: thesis: for x1 being Real st x1 in dom h & |.(x1 - x).| < s holds
|.((h . x1) - (h . x)).| < r
SS: r / 2 < r by XREAL_1:216, R0;
let x1 be Real; :: thesis: ( x1 in dom h & |.(x1 - x).| < s implies |.((h . x1) - (h . x)).| < r )
assume SC: ( x1 in dom h & |.(x1 - x).| < s ) ; :: thesis: |.((h . x1) - (h . x)).| < r

per cases then ( ( x1 in dom f & x1 in dom g ) or ( x1 in dom f & not x1 in dom g ) or x1 in dom g ) by FUNCT_4:12;

suppose ZT: ( x1 in dom f & x1 in dom g ) ; :: thesis: |.((h . x1) - (h . x)).| < r

i1: x1 in dom h by FUNCT_4:12, ZT;
then I1: x1 in dom (h | (dom f)) by ZT, RELAT_1:57;
s <= s2 by XXREAL_0:17;
then |.(x1 - x).| < s2 by XXREAL_0:2, SC;
then SD: |.(((h | (dom f)) . x1) - ((h | (dom f)) . x)).| < r / 2 by SB, i1, ZT, RELAT_1:57;
s1: (h | (dom f)) . x1 = h . x1 by FUNCT_1:47, I1;
(h | (dom f)) . x = h . x by FUNCT_1:47, SF;
hence |.((h . x1) - (h . x)).| < r by SS, XXREAL_0:2, SD, s1; :: thesis: verum

end;

suppose ZT: ( x1 in dom f & not x1 in dom g ) ; :: thesis: |.((h . x1) - (h . x)).| < r

then i1: x1 in dom h by FUNCT_4:12;
then I1: x1 in dom (h | (dom f)) by ZT, RELAT_1:57;
s <= s2 by XXREAL_0:17;
then |.(x1 - x).| < s2 by XXREAL_0:2, SC;
then SD: |.(((h | (dom f)) . x1) - ((h | (dom f)) . x)).| < r / 2 by SB, i1, ZT, RELAT_1:57;
s1: (h | (dom f)) . x1 = h . x1 by FUNCT_1:47, I1;
(h | (dom f)) . x = h . x by FUNCT_1:47, SF;
hence |.((h . x1) - (h . x)).| < r by SS, XXREAL_0:2, SD, s1; :: thesis: verum

end;

suppose P1: x1 in dom g ; :: thesis: |.((h . x1) - (h . x)).| < r

x1 in dom (h | (dom g)) by P1;
then P2: h . x1 = (h | (dom g)) . x1 by FUNCT_1:47;
P3: h . x = (h | (dom g)) . x by FUNCT_1:47, Sf;
s <= s1 by XXREAL_0:17;
then |.(x1 - x).| < s1 by XXREAL_0:2, SC;
then |.(((h | (dom g)) . x1) - ((h | (dom g)) . x)).| < r / 2 by Sb, P1;
hence |.((h . x1) - (h . x)).| < r by SS, XXREAL_0:2, P3, P2; :: thesis: verum

end;

end;

end;

hence h is_continuous_in x by FCONT_1:3; :: thesis: verum