let a, b be Real; :: thesis: ( id REAL is_integrable_on ['a,b'] & (id REAL) | ['a,b'] is bounded )
reconsider iR = id REAL as PartFunc of REAL,REAL ;
B1: iR | ['a,b'] is continuous ;
['a,b'] c= dom iR ;
hence ( id REAL is_integrable_on ['a,b'] & (id REAL) | ['a,b'] is bounded ) by INTEGRA5:11, INTEGRA5:10, B1; :: thesis: verum