let A be closed-interval Subset of REAL ; :: thesis: ( A = [.0 ,((PI * 3) / 2).] implies integral (sin - cos ),A = 2 )
assume A = [.0 ,((PI * 3) / 2).] ; :: thesis: integral (sin - cos ),A = 2
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 Th78
.= ((- (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:83
.= ((- 0 ) + 1) - ((- 1) - 0 ) by SIN_COS:81, SIN_COS:83 ;
hence integral (sin - cos ),A = 2 ; :: thesis: verum