let a, b be Real; :: thesis:
let f, g be PartFunc of REAL,REAL; :: thesis:
assume A1: ( g is continuous & not g is empty & f = (AffineMap (0,0)) | (REAL \ ].a,b.[) & dom g = [.a,b.] & g . a = 0 & g . b = 0 ) ; :: thesis:
then KK: f tolerates g by Asi1;
set c = b;
take h = f +* g; :: thesis:
thus h = f +* g ; :: thesis:
let x be Real; :: thesis:
U1: -infty < a by XXREAL_0:12, XREAL_0:def 1;
U3: b < +infty by XXREAL_0:9, XREAL_0:def 1;
REAL \ ].a,b.[ c= REAL ;
then REAL \ ].a,b.[ c= dom (AffineMap (0,0)) by FUNCT_2:def 1;
then S1: dom f = REAL \ ].a,b.[ by A1, RELAT_1:62;
aa: (REAL \ ].a,b.[) /\ [.a,b.] = (].-infty,a.] \/ [.b,+infty.[) /\ [.a,b.] by XXREAL_1:398
.= (].-infty,a.] /\ [.a,b.]) \/ ([.b,+infty.[ /\ [.a,b.]) by XBOOLE_1:23
.= {a} \/ ([.b,+infty.[ /\ [.a,b.]) by XXREAL_1:417, U1, XXREAL_1:29, A1
.= {a} \/ {b} by XXREAL_1:416, XXREAL_1:29, A1, U3
.= {a,b} by ENUMSET1:1 ;
a in (dom f) /\ (dom g) by aa, S1, A1, TARSKI:def 2;
then sx: ( a in dom f & a in dom g ) by XBOOLE_0:def 4;
nn: f . a = (AffineMap (0,0)) . a by FUNCT_1:47, A1, sx
.= (0 * a) + 0 by FCONT_1:def 4
.= 0 ;
b in (dom f) /\ (dom g) by aa, S1, A1, TARSKI:def 2;
then sy: ( b in dom f & b in dom g ) by XBOOLE_0:def 4;
then mn: f . b = (AffineMap (0,0)) . b by FUNCT_1:47, A1
.= (0 * b) + 0 by FCONT_1:def 4
.= 0 ;
Z7: dom f = ].-infty,a.] \/ [.b,+infty.[ by S1, XXREAL_1:398;
Z8: ].-infty,a.[ c= ].-infty,a.] by XXREAL_1:21;
xz: ].-infty,a.] c= dom f by XBOOLE_1:7, Z7;
then Z6: ].-infty,a.[ c= dom f by Z8;
z8: ].b,+infty.[ c= [.b,+infty.[ by XXREAL_1:22;
wz: [.b,+infty.[ c= dom f by XBOOLE_1:7, Z7;
then z6: ].b,+infty.[ c= dom f by z8;
assume x in dom h ; :: thesis:
then R1: ( x in dom f or x in dom g ) by FUNCT_4:12;
set xx0 = x;
b2: ].a,b.[ c= [.a,b.] by XXREAL_1:25;
b1: ].a,b.[ c= dom g by A1, XXREAL_1:25;
( x in ].-infty,a.] or x in [.b,+infty.[ or x in [.a,b.] ) by A1, R1, Z7, XBOOLE_0:def 3;
then ( x in ].-infty,a.[ \/ {a} or x in [.b,+infty.[ or x in [.a,b.] ) by XXREAL_1:423;
then ( x in ].-infty,a.[ or x in {a} or x in [.b,+infty.[ or x in [.a,b.] ) by XBOOLE_0:def 3;
then ( x in ].-infty,a.[ or x = a or x in {b} \/ ].b,+infty.[ or x in [.a,b.] ) by XXREAL_1:427, TARSKI:def 1;
then ( x in ].-infty,a.[ or x = a or x in {b} or x in ].b,+infty.[ or x in [.a,b.] ) by XBOOLE_0:def 3;
then ( x in ].-infty,a.[ or x = a or x = b or x in ].b,+infty.[ or x in {a,b} \/ ].a,b.[ ) by XXREAL_1:29, XXREAL_1:128, TARSKI:def 1;
then ( x in ].-infty,a.[ or x = a or x = b or x in ].b,+infty.[ or x in {a,b} or x in {a,b} or x in ].a,b.[ ) by XBOOLE_0:def 3;

per cases by TARSKI:def 2;

suppose FT: x = a ; :: thesis:

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:
assume H1: 0 < r ; :: thesis:
then consider s1 being Real such that
WW: ( 0 < s1 & ( for x1 being Real st x1 in dom g & |.(x1 - x).| < s1 holds
|.((g . x1) - (g . x)).| < r ) ) by FCONT_1:3, A1, sx, FT;
consider s2 being Real such that
W1: ( 0 < s2 & ( for x1 being Real st x1 in dom f & |.(x1 - x).| < s2 holds
|.((f . x1) - (f . x)).| < r ) ) by FCONT_1:3, H1, FCONT_1:def 2, A1, sx, FT;
take s = min (s1,s2); :: thesis:
thus 0 < s by WW, W1, XXREAL_0:15; :: thesis:
O2: ( s <= s1 & s <= s2 ) by XXREAL_0:17;
let x1 be Real; :: thesis:
assume O1: ( x1 in dom h & |.(x1 - x).| < s ) ; :: thesis:

per cases by FUNCT_4:12;

suppose W2: ( x1 in dom f & not x1 in dom g ) ; :: thesis:

then W3: h . x1 = f . x1 by FUNCT_4:11;
W4: h . x = f . x by A1, FT, nn, FUNCT_4:13, sx;
|.(x1 - x).| < s2 by O1, O2, XXREAL_0:2;
hence |.((h . x1) - (h . x)).| < r by W3, W4, W1, W2; :: thesis:

end;

suppose W2: ( x1 in dom f & x1 in dom g ) ; :: thesis:

then W3: h . x1 = g . x1 by FUNCT_4:13;
W4: h . x = g . x by FUNCT_4:13, sx, FT;
|.(x1 - x).| < s1 by O1, O2, XXREAL_0:2;
hence |.((h . x1) - (h . x)).| < r by W3, W4, W2, WW; :: thesis:

end;

suppose W2: x1 in dom g ; :: thesis:

then W3: h . x1 = g . x1 by FUNCT_4:13;
W4: h . x = g . x by FUNCT_4:13, FT, sx;
|.(x1 - x).| < s1 by O1, O2, XXREAL_0:2;
hence |.((h . x1) - (h . x)).| < r by W3, W4, W2, WW; :: thesis:

end;

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

end;

suppose FT: x = b ; :: thesis:

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:
assume H1: 0 < r ; :: thesis:
then consider s1 being Real such that
WW: ( 0 < s1 & ( for x1 being Real st x1 in dom g & |.(x1 - x).| < s1 holds
|.((g . x1) - (g . x)).| < r ) ) by FCONT_1:3, A1, sy, FT;
consider s2 being Real such that
W1: ( 0 < s2 & ( for x1 being Real st x1 in dom f & |.(x1 - x).| < s2 holds
|.((f . x1) - (f . x)).| < r ) ) by FCONT_1:3, H1, FCONT_1:def 2, A1, sy, FT;
take s = min (s1,s2); :: thesis:
thus 0 < s by WW, W1, XXREAL_0:15; :: thesis:
O2: ( s <= s1 & s <= s2 ) by XXREAL_0:17;
let x1 be Real; :: thesis:
assume O1: ( x1 in dom h & |.(x1 - x).| < s ) ; :: thesis:

per cases by FUNCT_4:12;

suppose W2: ( x1 in dom f & not x1 in dom g ) ; :: thesis:

then W3: h . x1 = f . x1 by FUNCT_4:11;
W4: h . x = f . x by mn, A1, FT, sy, FUNCT_4:13;
|.(x1 - x).| < s2 by O1, O2, XXREAL_0:2;
hence |.((h . x1) - (h . x)).| < r by W3, W4, W1, W2; :: thesis:

end;

suppose W2: ( x1 in dom f & x1 in dom g ) ; :: thesis:

then W3: h . x1 = g . x1 by FUNCT_4:13;
W4: h . x = g . x by FUNCT_4:13, sy, FT;
|.(x1 - x).| < s1 by O1, O2, XXREAL_0:2;
hence |.((h . x1) - (h . x)).| < r by W3, W4, W2, WW; :: thesis:

end;

suppose W2: x1 in dom g ; :: thesis:

then W3: h . x1 = g . x1 by FUNCT_4:13;
W4: h . x = g . x by FUNCT_4:13, FT, sy;
|.(x1 - x).| < s1 by O1, O2, XXREAL_0:2;
hence |.((h . x1) - (h . x)).| < r by W3, W4, W2, WW; :: thesis:

end;

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

end;

suppose B0: x in ].-infty,a.[ ; :: thesis:

for N1 being Neighbourhood of h . x ex N being Neighbourhood of x st
for x1 being Real st x1 in dom h & x1 in N holds
h . x1 in N1

proof

let N1 be Neighbourhood of h . x; :: thesis:
set r = h . x;
reconsider N2 = N1 as Neighbourhood of f . x by B0, Z8, xz, FUNCT_4:15, KK;
f is continuous by A1;
then consider Nx being Neighbourhood of x such that
D0: for x1 being Real st x1 in dom f & x1 in Nx holds
f . x1 in N2 by FCONT_1:4, B0, Z6;
set rr = a - x;
Zz: x + 0 < a by B0, XXREAL_1:233;
then Z1: a - x > 0 by XREAL_1:20;
set rr2 = (a - x) / 2;
set P1 = ].(x - ((a - x) / 2)),(x + ((a - x) / 2)).[;
x / 2 < a / 2 by Zz, XREAL_1:74;
then z5: (x / 2) + (a / 2) < (a / 2) + (a / 2) by XREAL_1:8;
].(x - ((a - x) / 2)),(x + ((a - x) / 2)).[ c= ].-infty,a.[ by XXREAL_1:263, z5;
then Y1: ].(x - ((a - x) / 2)),(x + ((a - x) / 2)).[ c= dom f by Z8, xz;
reconsider P1 = ].(x - ((a - x) / 2)),(x + ((a - x) / 2)).[ as Neighbourhood of x by Z1, RCOMP_1:def 6;
consider N being Neighbourhood of x such that
Y2: ( N c= Nx & N c= P1 ) by RCOMP_1:17;
take N ; :: thesis:
let x1 be Real; :: thesis:
assume D1: ( x1 in dom h & x1 in N ) ; :: thesis:
then f . x1 in N2 by D0, Y2, Y1;
hence h . x1 in N1 by FUNCT_4:15, Y2, Y1, D1, KK; :: thesis:

end;

hence h is_continuous_in x by FCONT_1:4; :: thesis:

end;

suppose B0: x in ].a,b.[ ; :: thesis:

for N1 being Neighbourhood of h . x ex N being Neighbourhood of x st
for x1 being Real st x1 in dom h & x1 in N holds
h . x1 in N1

proof

let N1 be Neighbourhood of h . x; :: thesis:
set r = h . x;
reconsider N2 = N1 as Neighbourhood of g . x by B0, A1, b2, FUNCT_4:13;
consider Nx being Neighbourhood of x such that
D0: for x1 being Real st x1 in dom g & x1 in Nx holds
g . x1 in N2 by FCONT_1:4, B0, b2, A1;
set rr = min ((x - a),(b - x));
Zw: ( a < x & x < b ) by B0, XXREAL_1:4;
( a - a < x - a & b - x > x - x ) by XREAL_1:14, Zw;
then Z1: min ((x - a),(b - x)) > 0 by XXREAL_0:15;
set rr2 = (min ((x - a),(b - x))) / 2;
set P1 = ].(x - ((min ((x - a),(b - x))) / 2)),(x + ((min ((x - a),(b - x))) / 2)).[;
u1: (min ((x - a),(b - x))) / 2 < min ((x - a),(b - x)) by Z1, XREAL_1:216;
u2: min ((x - a),(b - x)) <= b - x by XXREAL_0:17;
u3: x + ((min ((x - a),(b - x))) / 2) < x + (min ((x - a),(b - x))) by u1, XREAL_1:8;
x + (min ((x - a),(b - x))) <= x + (b - x) by u2, XREAL_1:7;
then Z5: x + ((min ((x - a),(b - x))) / 2) < b by u3, XXREAL_0:2;
min ((x - a),(b - x)) <= x - a by XXREAL_0:17;
then (min ((x - a),(b - x))) / 2 < x - a by XXREAL_0:2, u1;
then h1: x - ((min ((x - a),(b - x))) / 2) > x - (x - a) by XREAL_1:15;
y1: ].(x - ((min ((x - a),(b - x))) / 2)),(x + ((min ((x - a),(b - x))) / 2)).[ c= ].a,b.[ by XXREAL_1:46, Z5, h1;
reconsider P1 = ].(x - ((min ((x - a),(b - x))) / 2)),(x + ((min ((x - a),(b - x))) / 2)).[ as Neighbourhood of x by Z1, RCOMP_1:def 6;
consider N being Neighbourhood of x such that
Y2: ( N c= Nx & N c= P1 ) by RCOMP_1:17;
XX: N c= dom g by Y2, y1, b1;
take N ; :: thesis:
let x1 be Real; :: thesis:
assume D1: ( x1 in dom h & x1 in N ) ; :: thesis:
( x1 in Nx & x1 in dom g ) by Y2, y1, b1, D1;
then g . x1 in N2 by D0;
hence h . x1 in N1 by FUNCT_4:13, XX, D1; :: thesis:

end;

hence h is_continuous_in x by FCONT_1:4; :: thesis:

end;

suppose B0: x in ].b,+infty.[ ; :: thesis:

for N1 being Neighbourhood of h . x ex N being Neighbourhood of x st
for x1 being Real st x1 in dom h & x1 in N holds
h . x1 in N1

proof

let N1 be Neighbourhood of h . x; :: thesis:
set r = h . x;
reconsider N2 = N1 as Neighbourhood of f . x by B0, z6, FUNCT_4:15, A1, Asi1;
T1: f is continuous by A1;
consider Nx being Neighbourhood of x such that
D0: for x1 being Real st x1 in dom f & x1 in Nx holds
f . x1 in N2 by FCONT_1:4, B0, z6, T1;
set rr = x - b;
Zz: b + 0 < x by B0, XXREAL_1:235;
then Z1: x - b > 0 by XREAL_1:20;
set rr2 = (x - b) / 2;
set P1 = ].(x - ((x - b) / 2)),(x + ((x - b) / 2)).[;
Z3: b / 2 < x / 2 by Zz, XREAL_1:74;
(x / 2) + (b / 2) > (b / 2) + (b / 2) by Z3, XREAL_1:8;
then ].(x - ((x - b) / 2)),(x + ((x - b) / 2)).[ c= ].b,+infty.[ by XXREAL_1:247;
then Y1: ].(x - ((x - b) / 2)),(x + ((x - b) / 2)).[ c= dom f by z8, wz;
reconsider P1 = ].(x - ((x - b) / 2)),(x + ((x - b) / 2)).[ as Neighbourhood of x by Z1, RCOMP_1:def 6;
consider N being Neighbourhood of x such that
Y2: ( N c= Nx & N c= P1 ) by RCOMP_1:17;
take N ; :: thesis:
let x1 be Real; :: thesis:
assume D1: ( x1 in dom h & x1 in N ) ; :: thesis:
then f . x1 in N2 by D0, Y2, Y1;
hence h . x1 in N1 by FUNCT_4:15, Y2, Y1, D1, KK; :: thesis:

end;

hence h is_continuous_in x by FCONT_1:4; :: thesis:

end;