let A be closed-interval Subset of REAL ; :: thesis: ( exp_R is_integrable_on A & exp_R | A is bounded )
X: A c= dom exp_R by D4;
exp_R | A is continuous ;
hence ( exp_R is_integrable_on A & exp_R | A is bounded ) by X, INTEGRA5:10, INTEGRA5:11; :: thesis: verum