let A be non empty closed_interval Subset of REAL; :: thesis: ( exp_R (#) (sin + cos) is_integrable_on A & (exp_R (#) (sin + cos)) | A is bounded )
A1: dom (sin + cos) = (dom sin) /\ (dom cos) by VALUED_1:def 1;
( dom sin = REAL & dom cos = REAL ) by FUNCT_2:def 1;
then A c= (dom exp_R) /\ (dom (sin + cos)) by A1, SIN_COS:47;
then A2: A c= dom (exp_R (#) (sin + cos)) by VALUED_1:def 4;
(exp_R (#) (sin + cos)) | A is continuous ;
hence ( exp_R (#) (sin + cos) is_integrable_on A & (exp_R (#) (sin + cos)) | A is bounded ) by A2, INTEGRA5:10, INTEGRA5:11; :: thesis: verum