let A be non empty closed_interval Subset of REAL; :: thesis: for f being Function of REAL,REAL st f is_integrable_on A & f | A is bounded holds
( (id REAL) (#) f is_integrable_on A & ((id REAL) (#) f) | A is bounded )
let f be Function of REAL,REAL; :: thesis: ( f is_integrable_on A & f | A is bounded implies ( (id REAL) (#) f is_integrable_on A & ((id REAL) (#) f) | A is bounded ) )
assume A1: ( f is_integrable_on A & f | A is bounded ) ; :: thesis: ( (id REAL) (#) f is_integrable_on A & ((id REAL) (#) f) | A is bounded )
A4: dom f = REAL by FUNCT_2:def 1;
reconsider f = f as PartFunc of REAL,REAL ;
A2: ( f is_integrable_on A & f | A is bounded ) by A1;
reconsider iR = id REAL as PartFunc of REAL,REAL ;
A3: A c= dom iR ;
B1: iR is_integrable_on A by Lm2;
iR | A is bounded by Lm2;
hence ( (id REAL) (#) f is_integrable_on A & ((id REAL) (#) f) | A is bounded ) by INTEGRA6:14, A2, A4, B1, A3, INTEGRA6:13; :: thesis: verum