let A be non empty closed_interval Subset of REAL; :: thesis: for f being Function of REAL,REAL st f is continuous holds
( f is_integrable_on A & f | A is bounded )
let f be Function of REAL,REAL; :: thesis: ( f is continuous implies ( f is_integrable_on A & f | A is bounded ) )
assume A1: f is continuous ; :: thesis: ( f is_integrable_on A & f | A is bounded )
DD: REAL = dom f by FUNCT_2:def 1;
reconsider ff = f as PartFunc of REAL,REAL ;
ff | A is continuous by A1;
hence ( f is_integrable_on A & f | A is bounded ) by INTEGRA5:11, INTEGRA5:10, DD; :: thesis: verum