let A be non empty closed_interval Subset of REAL; :: thesis: ( A = [.0,PI.] implies integral ((sin (#) cos),A) = 0 )
assume A = [.0,PI.] ; :: thesis: integral ((sin (#) cos),A) = 0
then ( upper_bound A = PI & lower_bound A = 0 ) by Th37;
then integral ((sin (#) cos),A) = (1 / 2) * (((cos . 0) * (cos . 0)) - ((cos . PI) * (cos . PI))) by Th90
.= (1 / 2) * (((cos . (0 + (2 * PI))) * (cos . 0)) - ((cos . PI) * (cos . PI))) by SIN_COS:78
.= (1 / 2) * ((1 * 1) - ((- 1) * (- 1))) by SIN_COS:76, SIN_COS:78 ;
hence integral ((sin (#) cos),A) = 0 ; :: thesis: verum