let A be non empty closed_interval Subset of REAL; :: thesis: ( id REAL is_integrable_on A & (id REAL) | A is bounded )
reconsider iR = id REAL as PartFunc of REAL,REAL ;
B1: iR | A is continuous ;
A c= dom iR ;
hence ( id REAL is_integrable_on A & (id REAL) | A is bounded ) by INTEGRA5:11, INTEGRA5:10, B1; :: thesis: verum