let a, b, c be Real; :: thesis: for f, g being Function of ['a,c'],REAL st a <= b & b <= c & f | ['a,c'] is bounded & g | ['a,c'] is bounded holds
((f | [.a,b.]) +* (g | [.b,c.])) | ['a,c'] is bounded
let f, g be Function of ['a,c'],REAL; :: thesis: ( a <= b & b <= c & f | ['a,c'] is bounded & g | ['a,c'] is bounded implies ((f | [.a,b.]) +* (g | [.b,c.])) | ['a,c'] is bounded )
assume A1: ( a <= b & b <= c ) ; :: thesis: ( not f | ['a,c'] is bounded or not g | ['a,c'] is bounded or ((f | [.a,b.]) +* (g | [.b,c.])) | ['a,c'] is bounded )
assume A2: ( f | ['a,c'] is bounded & g | ['a,c'] is bounded ) ; :: thesis: ((f | [.a,b.]) +* (g | [.b,c.])) | ['a,c'] is bounded
set g1 = f | [.a,b.];
set g2 = g | [.b,c.];
set h = (f | [.a,b.]) +* (g | [.b,c.]);
ex r being Real st
for y being set st y in dom (((f | [.a,b.]) +* (g | [.b,c.])) | ['a,c']) holds
|.((((f | [.a,b.]) +* (g | [.b,c.])) | ['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, A2;
take max (r,r1) ; :: thesis: for y being set st y in dom (((f | [.a,b.]) +* (g | [.b,c.])) | ['a,c']) holds
|.((((f | [.a,b.]) +* (g | [.b,c.])) | ['a,c']) . y).| < max (r,r1)
for x being set st x in dom (((f | [.a,b.]) +* (g | [.b,c.])) | ['a,c']) holds
|.((((f | [.a,b.]) +* (g | [.b,c.])) | ['a,c']) . x).| < max (r,r1)

proof

let x be set ; :: thesis: ( x in dom (((f | [.a,b.]) +* (g | [.b,c.])) | ['a,c']) implies |.((((f | [.a,b.]) +* (g | [.b,c.])) | ['a,c']) . x).| < max (r,r1) )
assume B1: x in dom (((f | [.a,b.]) +* (g | [.b,c.])) | ['a,c']) ; :: thesis: |.((((f | [.a,b.]) +* (g | [.b,c.])) | ['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: |.((((f | [.a,b.]) +* (g | [.b,c.])) | ['a,c']) . x).| < max (r,r1)

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

end;

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

then D3: x in [.b,c.] by BB2;
dom g = ['a,c'] by FUNCT_2:def 1
.= [.a,c.] by INTEGRA5:def 3, XXREAL_0:2, A1 ;
then D4: x in dom (g | [.b,c.]) by D3, RELAT_1:62, XXREAL_1:34, A1;
E2: |.((((f | [.a,b.]) +* (g | [.b,c.])) | ['a,c']) . x).| = |.((g | [.b,c.]) . x).| by FUNCT_4:13, D4
.= |.((g | ['a,c']) . x).| by FUNCT_1:49, BB2, XXREAL_1:1, S2 ;
r1 <= max (r,r1) by XXREAL_0:25;
hence |.((((f | [.a,b.]) +* (g | [.b,c.])) | ['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 (((f | [.a,b.]) +* (g | [.b,c.])) | ['a,c']) holds
|.((((f | [.a,b.]) +* (g | [.b,c.])) | ['a,c']) . y).| < max (r,r1) ; :: thesis: verum

end;

hence ((f | [.a,b.]) +* (g | [.b,c.])) | ['a,c'] is bounded by COMSEQ_2:def 3; :: thesis: verum