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 ( f | A is bounded & g | A is bounded ) ; :: thesis: ((f | ].-infty,c.]) +* (g | [.c,+infty.[)) | A is bounded
then ((f | ].-infty,c.[) +* (g | [.c,+infty.[)) | A is bounded by Th18X;
hence ((f | ].-infty,c.]) +* (g | [.c,+infty.[)) | A is bounded by Th18E; :: thesis: verum