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