let A be closed-interval Subset of REAL ; :: thesis: ( exp_R (#) (sin + cos ) is_integrable_on A & (exp_R (#) (sin + cos )) | A is bounded )
W: ( dom sin = REAL & dom cos = REAL ) by FUNCT_2:def 1;
A: dom (sin + cos ) = (dom sin ) /\ (dom cos ) by VALUED_1:def 1;
dom exp_R = REAL by SIN_COS:51;
then A c= (dom exp_R ) /\ (dom (sin + cos )) by A, W;
then V: 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 V, INTEGRA5:10, INTEGRA5:11; :: thesis: verum