let A be closed-interval Subset of REAL ; :: thesis: integral (sin (#) sin ),A = (((cos . (lower_bound A)) * (sin . (lower_bound A))) - ((cos . (upper_bound A)) * (sin . (upper_bound A)))) + (integral (cos (#) cos ),A)
X: A c= dom sin by D1;
sin | A is continuous ;
then A1: ( (- cos ) `| REAL is_integrable_on A & ((- cos ) `| REAL ) | A is bounded ) by Th29, X, INTEGRA5:10, INTEGRA5:11;
Y: A c= dom cos by D2;
cos | A is continuous ;
then A2: ( sin `| REAL is_integrable_on A & (sin `| REAL ) | A is bounded ) by Th27, Y, INTEGRA5:10, INTEGRA5:11;
( cos (#) cos is_integrable_on A & (cos (#) cos ) | A is bounded ) by Lm17;
then A3: ( (cos (#) cos ) || A is integrable & ((cos (#) cos ) || A) | A is bounded ) by INTEGRA5:9, INTEGRA5:def 2;
dom (cos (#) cos ) = REAL by FUNCT_2:def 1;
then A4: (cos (#) cos ) || A is Function of A,REAL by FUNCT_2:131, INTEGRA5:6;
[#] REAL is open Subset of REAL ;
then integral (sin (#) sin ),A = ((((- cos ) . (upper_bound A)) * (sin . (upper_bound A))) - (((- cos ) . (lower_bound A)) * (sin . (lower_bound A)))) - (integral ((- cos ) (#) cos ),A) by A1, A2, Th26, Th27, Th29, INTEGRA5:21, SIN_COS:73
.= (((- (cos . (upper_bound A))) * (sin . (upper_bound A))) - (((- cos ) . (lower_bound A)) * (sin . (lower_bound A)))) - (integral ((- cos ) (#) cos ),A) by VALUED_1:8
.= (((- (cos . (upper_bound A))) * (sin . (upper_bound A))) - ((- (cos . (lower_bound A))) * (sin . (lower_bound A)))) - (integral ((- cos ) (#) cos ),A) by VALUED_1:8
.= (((cos . (lower_bound A)) * (sin . (lower_bound A))) - ((cos . (upper_bound A)) * (sin . (upper_bound A)))) - (integral (- (cos (#) cos )),A) by RFUNCT_1:24
.= (((cos . (lower_bound A)) * (sin . (lower_bound A))) - ((cos . (upper_bound A)) * (sin . (upper_bound A)))) - (integral ((- 1) (#) ((cos (#) cos ) || A))) by RFUNCT_1:65
.= (((cos . (lower_bound A)) * (sin . (lower_bound A))) - ((cos . (upper_bound A)) * (sin . (upper_bound A)))) - ((- 1) * (integral (cos (#) cos ),A)) by A3, A4, INTEGRA2:31
.= (((cos . (lower_bound A)) * (sin . (lower_bound A))) - ((cos . (upper_bound A)) * (sin . (upper_bound A)))) + (integral (cos (#) cos ),A) ;
hence integral (sin (#) sin ),A = (((cos . (lower_bound A)) * (sin . (lower_bound A))) - ((cos . (upper_bound A)) * (sin . (upper_bound A)))) + (integral (cos (#) cos ),A) ; :: thesis: verum