let A be non empty closed_interval Subset of REAL; :: thesis: for a being Real
for f, g being Function of REAL,REAL st f | A is bounded & g | A is bounded & a in A holds
( ((f | ].-infty,a.[) +* (g | [.a,+infty.[)) | ['(lower_bound A),a'] is bounded & ((f | ].-infty,a.[) +* (g | [.a,+infty.[)) | ['a,(upper_bound A)'] is bounded )
let a be Real; :: thesis: for f, g being Function of REAL,REAL st f | A is bounded & g | A is bounded & a in A holds
( ((f | ].-infty,a.[) +* (g | [.a,+infty.[)) | ['(lower_bound A),a'] is bounded & ((f | ].-infty,a.[) +* (g | [.a,+infty.[)) | ['a,(upper_bound A)'] is bounded )
let f, g be Function of REAL,REAL; :: thesis: ( f | A is bounded & g | A is bounded & a in A implies ( ((f | ].-infty,a.[) +* (g | [.a,+infty.[)) | ['(lower_bound A),a'] is bounded & ((f | ].-infty,a.[) +* (g | [.a,+infty.[)) | ['a,(upper_bound A)'] is bounded ) )
assume that
A1: f | A is bounded and
A2: g | A is bounded and
A3: a in A ; :: thesis: ( ((f | ].-infty,a.[) +* (g | [.a,+infty.[)) | ['(lower_bound A),a'] is bounded & ((f | ].-infty,a.[) +* (g | [.a,+infty.[)) | ['a,(upper_bound A)'] is bounded )
a in [.(lower_bound A),(upper_bound A).] by INTEGRA1:4, A3;
then A31: ( lower_bound A <= a & a <= upper_bound A ) by XXREAL_1:1;
set F = (f | ].-infty,a.[) +* (g | [.a,+infty.[);
set LBa = ['(lower_bound A),a'];
set aUB = ['a,(upper_bound A)'];
BO: ex r being Real st
for y being set st y in dom (((f | ].-infty,a.[) +* (g | [.a,+infty.[)) | ['(lower_bound A),a']) holds
|.((((f | ].-infty,a.[) +* (g | [.a,+infty.[)) | ['(lower_bound A),a']) . y).| < r

proof

consider r being Real such that
C1: for y being set st y in dom (f | A) holds
|.((f | A) . y).| < r by COMSEQ_2:def 3, A1;
consider r1 being Real such that
C2: for y being set st y in dom (g | A) holds
|.((g | A) . y).| < r1 by COMSEQ_2:def 3, A2;
take max (r,r1) ; :: thesis: for y being set st y in dom (((f | ].-infty,a.[) +* (g | [.a,+infty.[)) | ['(lower_bound A),a']) holds
|.((((f | ].-infty,a.[) +* (g | [.a,+infty.[)) | ['(lower_bound A),a']) . y).| < max (r,r1)
for x being set st x in dom (((f | ].-infty,a.[) +* (g | [.a,+infty.[)) | ['(lower_bound A),a']) holds
|.((((f | ].-infty,a.[) +* (g | [.a,+infty.[)) | ['(lower_bound A),a']) . x).| < max (r,r1)

proof

let x be set ; :: thesis: ( x in dom (((f | ].-infty,a.[) +* (g | [.a,+infty.[)) | ['(lower_bound A),a']) implies |.((((f | ].-infty,a.[) +* (g | [.a,+infty.[)) | ['(lower_bound A),a']) . x).| < max (r,r1) )
assume x in dom (((f | ].-infty,a.[) +* (g | [.a,+infty.[)) | ['(lower_bound A),a']) ; :: thesis: |.((((f | ].-infty,a.[) +* (g | [.a,+infty.[)) | ['(lower_bound A),a']) . x).| < max (r,r1)
then B1: x in ['(lower_bound A),a'] by RELAT_1:57;
D1: A = dom (f | A) by FUNCT_2:def 1;
D2: A = dom (g | A) by FUNCT_2:def 1;
reconsider x = x as Real by B1;
x in [.(lower_bound A),a.] by INTEGRA5:def 3, B1, A31;
then ( lower_bound A <= x & x <= a ) by XXREAL_1:1;
then ( lower_bound A <= x & x <= upper_bound A ) by XXREAL_0:2, A31;
then x in [.(lower_bound A),(upper_bound A).] ;
then B11: x in A by INTEGRA1:4;

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

suppose S1: x < a ; :: thesis: |.((((f | ].-infty,a.[) +* (g | [.a,+infty.[)) | ['(lower_bound A),a']) . x).| < max (r,r1)

then B4: not x in dom (g | [.a,+infty.[) by XXREAL_1:236;
E1: |.((((f | ].-infty,a.[) +* (g | [.a,+infty.[)) | ['(lower_bound A),a']) . x).| = |.(((f | ].-infty,a.[) +* (g | [.a,+infty.[)) . x).| by FUNCT_1:49, B1
.= |.((f | ].-infty,a.[) . x).| by FUNCT_4:11, B4
.= |.(f . x).| by FUNCT_1:49, XXREAL_1:233, S1
.= |.((f | A) . x).| by FUNCT_1:49, B11 ;
r <= max (r,r1) by XXREAL_0:25;
hence |.((((f | ].-infty,a.[) +* (g | [.a,+infty.[)) | ['(lower_bound A),a']) . x).| < max (r,r1) by XXREAL_0:2, E1, C1, D1, B11; :: thesis: verum

end;

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

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

end;

end;

end;

hence for y being set st y in dom (((f | ].-infty,a.[) +* (g | [.a,+infty.[)) | ['(lower_bound A),a']) holds
|.((((f | ].-infty,a.[) +* (g | [.a,+infty.[)) | ['(lower_bound A),a']) . y).| < max (r,r1) ; :: thesis: verum

end;

ex r being Real st
for y being set st y in dom (((f | ].-infty,a.[) +* (g | [.a,+infty.[)) | ['a,(upper_bound A)']) holds
|.((((f | ].-infty,a.[) +* (g | [.a,+infty.[)) | ['a,(upper_bound A)']) . y).| < r

proof

consider r being Real such that
C1: for y being set st y in dom (f | A) holds
|.((f | A) . y).| < r by COMSEQ_2:def 3, A1;
consider r1 being Real such that
C2: for y being set st y in dom (g | A) holds
|.((g | A) . y).| < r1 by COMSEQ_2:def 3, A2;
take max (r,r1) ; :: thesis: for y being set st y in dom (((f | ].-infty,a.[) +* (g | [.a,+infty.[)) | ['a,(upper_bound A)']) holds
|.((((f | ].-infty,a.[) +* (g | [.a,+infty.[)) | ['a,(upper_bound A)']) . y).| < max (r,r1)
for x being set st x in dom (((f | ].-infty,a.[) +* (g | [.a,+infty.[)) | ['a,(upper_bound A)']) holds
|.((((f | ].-infty,a.[) +* (g | [.a,+infty.[)) | ['a,(upper_bound A)']) . x).| < max (r,r1)

proof

let x be set ; :: thesis: ( x in dom (((f | ].-infty,a.[) +* (g | [.a,+infty.[)) | ['a,(upper_bound A)']) implies |.((((f | ].-infty,a.[) +* (g | [.a,+infty.[)) | ['a,(upper_bound A)']) . x).| < max (r,r1) )
assume x in dom (((f | ].-infty,a.[) +* (g | [.a,+infty.[)) | ['a,(upper_bound A)']) ; :: thesis: |.((((f | ].-infty,a.[) +* (g | [.a,+infty.[)) | ['a,(upper_bound A)']) . x).| < max (r,r1)
then B1: x in ['a,(upper_bound A)'] by RELAT_1:57;
then reconsider x = x as Real ;
D1: A = dom (f | A) by FUNCT_2:def 1;
D2: A = dom (g | A) by FUNCT_2:def 1;
x in [.a,(upper_bound A).] by INTEGRA5:def 3, B1, A31;
then ( a <= x & x <= upper_bound A ) by XXREAL_1:1;
then ( lower_bound A <= x & x <= upper_bound A ) by XXREAL_0:2, A31;
then x in [.(lower_bound A),(upper_bound A).] ;
then B11: x in A by INTEGRA1:4;

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

suppose S1: x < a ; :: thesis: |.((((f | ].-infty,a.[) +* (g | [.a,+infty.[)) | ['a,(upper_bound A)']) . x).| < max (r,r1)

then B4: not x in dom (g | [.a,+infty.[) by XXREAL_1:236;
E1: |.((((f | ].-infty,a.[) +* (g | [.a,+infty.[)) | ['a,(upper_bound A)']) . x).| = |.(((f | ].-infty,a.[) +* (g | [.a,+infty.[)) . x).| by FUNCT_1:49, B1
.= |.((f | ].-infty,a.[) . x).| by FUNCT_4:11, B4
.= |.(f . x).| by FUNCT_1:49, XXREAL_1:233, S1
.= |.((f | A) . x).| by FUNCT_1:49, B11 ;
r <= max (r,r1) by XXREAL_0:25;
hence |.((((f | ].-infty,a.[) +* (g | [.a,+infty.[)) | ['a,(upper_bound A)']) . x).| < max (r,r1) by XXREAL_0:2, E1, C1, D1, B11; :: thesis: verum

end;

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

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

end;

end;

end;

hence for y being set st y in dom (((f | ].-infty,a.[) +* (g | [.a,+infty.[)) | ['a,(upper_bound A)']) holds
|.((((f | ].-infty,a.[) +* (g | [.a,+infty.[)) | ['a,(upper_bound A)']) . y).| < max (r,r1) ; :: thesis: verum

end;

hence ( ((f | ].-infty,a.[) +* (g | [.a,+infty.[)) | ['(lower_bound A),a'] is bounded & ((f | ].-infty,a.[) +* (g | [.a,+infty.[)) | ['a,(upper_bound A)'] is bounded ) by BO, COMSEQ_2:def 3; :: thesis: verum