let A be non empty closed_interval Subset of REAL; :: thesis: for c being Real
for f, g being Function of REAL,REAL st f | A is bounded & g | A is bounded holds
((f | ].-infty,c.[) +* (g | [.c,+infty.[)) | A is bounded
let c be Real; :: thesis: for f, g being Function of REAL,REAL st f | A is bounded & g | A is bounded holds
((f | ].-infty,c.[) +* (g | [.c,+infty.[)) | A is bounded
let f, g be Function of REAL,REAL; :: thesis: ( f | A is bounded & g | A is bounded implies ((f | ].-infty,c.[) +* (g | [.c,+infty.[)) | A is bounded )
assume that
A2: f | A is bounded and
A4: g | A is bounded ; :: thesis: ((f | ].-infty,c.[) +* (g | [.c,+infty.[)) | A is bounded
set F = (f | ].-infty,c.[) +* (g | [.c,+infty.[);
reconsider F = (f | ].-infty,c.[) +* (g | [.c,+infty.[) as Function of REAL,REAL by Th19;
ex r being Real st
for y being set st y in dom (F | A) holds
|.((F | 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, A2;
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, A4;
take max (r,r1) ; :: thesis: for y being set st y in dom (F | A) holds
|.((F | A) . y).| < max (r,r1)
for x being set st x in dom (F | A) holds
|.((F | A) . x).| < max (r,r1)

proof

let x be set ; :: thesis: ( x in dom (F | A) implies |.((F | A) . x).| < max (r,r1) )
assume B1: x in dom (F | A) ; :: thesis: |.((F | A) . x).| < max (r,r1)
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;

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

suppose S1: x < c ; :: thesis: |.((F | A) . x).| < max (r,r1)

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

end;

suppose S2: x >= c ; :: thesis: |.((F | A) . x).| < max (r,r1)

then x in [.c,+infty.[ by XXREAL_1:236;
then D4: x in dom (g | [.c,+infty.[) by FUNCT_2:def 1;
E2: |.((F | A) . x).| = |.(F . x).| by FUNCT_1:49, B1
.= |.((g | [.c,+infty.[) . x).| by FUNCT_4:13, D4
.= |.(g . x).| by FUNCT_1:49, XXREAL_1:236, S2
.= |.((g | A) . x).| by FUNCT_1:49, B1 ;
r1 <= max (r,r1) by XXREAL_0:25;
hence |.((F | A) . 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) holds
|.((F | A) . y).| < max (r,r1) ; :: thesis: verum

end;

hence ((f | ].-infty,c.[) +* (g | [.c,+infty.[)) | A is bounded by COMSEQ_2:def 3; :: thesis: verum