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