let A be non empty 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 Th78
.= ((- (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:78
.= ((- 1) + 1) - (0 - 0) by SIN_COS:76, SIN_COS:78 ;
hence integral ((sin - cos),A) = 0 ; :: thesis: verum