let A be closed-interval Subset of REAL ; :: thesis: integral (sin (#) cos ),A = (1 / 2) * (((cos . (lower_bound A)) * (cos . (lower_bound A))) - ((cos . (upper_bound A)) * (cos . (upper_bound A))))
Y: A c= dom sin by D1;
W: A c= dom (- sin ) by D3;
sin | A is continuous ;
then A1: ( (- cos ) `| REAL is_integrable_on A & ((- cos ) `| REAL ) | A is bounded ) by Th29, Y, INTEGRA5:10, INTEGRA5:11;
(- sin ) | A is continuous ;
then A2: ( cos `| REAL is_integrable_on A & (cos `| REAL ) | A is bounded ) by Th28, W, INTEGRA5:10, INTEGRA5:11;
[#] REAL is open Subset of REAL ;
then integral (sin (#) cos ),A = ((((- cos ) . (upper_bound A)) * (cos . (upper_bound A))) - (((- cos ) . (lower_bound A)) * (cos . (lower_bound A)))) - (integral ((- cos ) (#) (- sin )),A) by A1, A2, Th26, Th28, Th29, INTEGRA5:21, SIN_COS:72
.= ((((- cos ) . (upper_bound A)) * (cos . (upper_bound A))) - (((- cos ) . (lower_bound A)) * (cos . (lower_bound A)))) - (integral (sin (#) cos ),A) by Lm4
.= (((- (cos . (upper_bound A))) * (cos . (upper_bound A))) - (((- cos ) . (lower_bound A)) * (cos . (lower_bound A)))) - (integral (sin (#) cos ),A) by VALUED_1:8
.= (((- (cos . (upper_bound A))) * (cos . (upper_bound A))) - ((- (cos . (lower_bound A))) * (cos . (lower_bound A)))) - (integral (sin (#) cos ),A) by VALUED_1:8
.= (((cos . (lower_bound A)) * (cos . (lower_bound A))) - ((cos . (upper_bound A)) * (cos . (upper_bound A)))) - (integral (sin (#) cos ),A) ;
hence integral (sin (#) cos ),A = (1 / 2) * (((cos . (lower_bound A)) * (cos . (lower_bound A))) - ((cos . (upper_bound A)) * (cos . (upper_bound A)))) ; :: thesis: verum