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