let A be non empty closed_interval Subset of REAL; :: thesis: for r1, r2 being Real
for f being Function of REAL,REAL st f is_integrable_on A & f | A is bounded holds
( min ((AffineMap (0,r1)),(r2 (#) f)) is_integrable_on A & (min ((AffineMap (0,r1)),(r2 (#) f))) | A is bounded )
let r1, r2 be Real; :: thesis: for f being Function of REAL,REAL st f is_integrable_on A & f | A is bounded holds
( min ((AffineMap (0,r1)),(r2 (#) f)) is_integrable_on A & (min ((AffineMap (0,r1)),(r2 (#) f))) | A is bounded )
let f be Function of REAL,REAL; :: thesis: ( f is_integrable_on A & f | A is bounded implies ( min ((AffineMap (0,r1)),(r2 (#) f)) is_integrable_on A & (min ((AffineMap (0,r1)),(r2 (#) f))) | A is bounded ) )
assume that
A2: f is_integrable_on A and
A3: f | A is bounded ; :: thesis: ( min ((AffineMap (0,r1)),(r2 (#) f)) is_integrable_on A & (min ((AffineMap (0,r1)),(r2 (#) f))) | A is bounded )
A c= REAL ;
then Df: A c= dom f by FUNCT_2:def 1;
A c= REAL ;
then B21: A c= dom (AffineMap (0,r1)) by FUNCT_2:def 1;
set F3 = AffineMap (0,r1);
reconsider f = f, F3 = AffineMap (0,r1) as PartFunc of REAL,REAL ;
C1: F3 | A is continuous ;
A23: ( f is_integrable_on A & f | A is bounded ) by A2, A3;
reconsider f = f, F3 = F3 as Function of REAL,REAL ;
( F3 is_integrable_on A & F3 | A is bounded & r2 (#) f is_integrable_on A & (r2 (#) f) | A is bounded ) by INTEGRA6:9, Df, A23, RFUNCT_1:80, C1, INTEGRA5:10, INTEGRA5:11, B21;
hence ( min ((AffineMap (0,r1)),(r2 (#) f)) is_integrable_on A & (min ((AffineMap (0,r1)),(r2 (#) f))) | A is bounded ) by Th12; :: thesis: verum