let a, b, c be Real; :: thesis: for f, g, h being Function of REAL,REAL st a <= b & b <= c & f | ['a,c'] is bounded & g | ['a,c'] is bounded & h = (f | [.a,b.]) +* (g | [.b,c.]) & f . b = g . b holds
h | ['a,c'] is bounded
let f, g, h be Function of REAL,REAL; :: thesis: ( a <= b & b <= c & f | ['a,c'] is bounded & g | ['a,c'] is bounded & h = (f | [.a,b.]) +* (g | [.b,c.]) & f . b = g . b implies h | ['a,c'] is bounded )
assume that
A1: ( a <= b & b <= c ) and
A2: f | ['a,c'] is bounded and
A3: g | ['a,c'] is bounded and
A4: h = (f | [.a,b.]) +* (g | [.b,c.]) and
A5: f . b = g . b ; :: thesis: h | ['a,c'] is bounded
B10: f | [.a,b.] tolerates g | [.b,c.]

proof

for x being object st x in (dom (f | [.a,b.])) /\ (dom (g | [.b,c.])) holds
(f | [.a,b.]) . x = (g | [.b,c.]) . x

proof

let x be object ; :: thesis: ( x in (dom (f | [.a,b.])) /\ (dom (g | [.b,c.])) implies (f | [.a,b.]) . x = (g | [.b,c.]) . x )
assume T1: x in (dom (f | [.a,b.])) /\ (dom (g | [.b,c.])) ; :: thesis: (f | [.a,b.]) . x = (g | [.b,c.]) . x
T2: (dom (f | [.a,b.])) /\ (dom (g | [.b,c.])) = [.a,b.] /\ (dom (g | [.b,c.])) by FUNCT_2:def 1
.= [.a,b.] /\ [.b,c.] by FUNCT_2:def 1
.= {b} by XXREAL_1:418, A1 ;
then (f | [.a,b.]) . x = (f | [.a,b.]) . b by TARSKI:def 1, T1
.= g . b by A5, FUNCT_1:49, XXREAL_1:1, A1
.= (g | [.b,c.]) . b by FUNCT_1:49, XXREAL_1:1, A1 ;
hence (f | [.a,b.]) . x = (g | [.b,c.]) . x by TARSKI:def 1, T1, T2; :: thesis: verum

end;

hence f | [.a,b.] tolerates g | [.b,c.] by PARTFUN1:def 4; :: thesis: verum

end;

ex r being Real st
for y being set st y in dom (h | ['a,c']) holds
|.((h | ['a,c']) . y).| < r

proof

consider r being Real such that
C1: for y being set st y in dom (f | ['a,c']) holds
|.((f | ['a,c']) . y).| < r by COMSEQ_2:def 3, A2;
consider r1 being Real such that
C2: for y being set st y in dom (g | ['a,c']) holds
|.((g | ['a,c']) . y).| < r1 by COMSEQ_2:def 3, A3;
take max (r,r1) ; :: thesis: for y being set st y in dom (h | ['a,c']) holds
|.((h | ['a,c']) . y).| < max (r,r1)
for x being set st x in dom (h | ['a,c']) holds
|.((h | ['a,c']) . x).| < max (r,r1)

proof

let x be set ; :: thesis: ( x in dom (h | ['a,c']) implies |.((h | ['a,c']) . x).| < max (r,r1) )
assume B1: x in dom (h | ['a,c']) ; :: thesis: |.((h | ['a,c']) . x).| < max (r,r1)
D1: ['a,c'] = dom (f | ['a,c']) by FUNCT_2:def 1;
D2: ['a,c'] = dom (g | ['a,c']) by FUNCT_2:def 1;
B2: x in ['a,c'] by B1;
reconsider x = x as Real by B1;
x in [.a,c.] by INTEGRA5:def 3, A1, XXREAL_0:2, B2;
then BB2: ( a <= x & x <= c ) by XXREAL_1:1;

per cases ( x < b or x >= b ) ;

suppose S1: x < b ; :: thesis: |.((h | ['a,c']) . x).| < max (r,r1)

then x in [.a,b.] by BB2;
then B4: x in dom (f | [.a,b.]) by FUNCT_2:def 1;
E1: |.((h | ['a,c']) . x).| = |.(((f | [.a,b.]) +* (g | [.b,c.])) . x).| by A4, FUNCT_1:49, B1
.= |.((f | [.a,b.]) . x).| by FUNCT_4:15, B4, B10
.= |.(f . x).| by FUNCT_1:49, XXREAL_1:1, BB2, S1
.= |.((f | ['a,c']) . x).| by FUNCT_1:49, B1 ;
r <= max (r,r1) by XXREAL_0:25;
hence |.((h | ['a,c']) . x).| < max (r,r1) by XXREAL_0:2, E1, C1, B1, D1; :: thesis: verum

end;

suppose S2: x >= b ; :: thesis: |.((h | ['a,c']) . x).| < max (r,r1)

then x in [.b,c.] by BB2;
then D4: x in dom (g | [.b,c.]) by FUNCT_2:def 1;
E2: |.((h | ['a,c']) . x).| = |.(((f | [.a,b.]) +* (g | [.b,c.])) . x).| by A4, FUNCT_1:49, B1
.= |.((g | [.b,c.]) . x).| by FUNCT_4:13, D4
.= |.(g . x).| by FUNCT_1:49, BB2, XXREAL_1:1, S2
.= |.((g | ['a,c']) . x).| by FUNCT_1:49, B1 ;
r1 <= max (r,r1) by XXREAL_0:25;
hence |.((h | ['a,c']) . x).| < max (r,r1) by XXREAL_0:2, C2, B1, D2, E2; :: thesis: verum

end;

end;

end;

hence for y being set st y in dom (h | ['a,c']) holds
|.((h | ['a,c']) . y).| < max (r,r1) ; :: thesis: verum

end;

hence h | ['a,c'] is bounded by COMSEQ_2:def 3; :: thesis: verum