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