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