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