let A be closed-interval Subset of REAL ; integral (sin (#) sin ),A = (((cos . (lower_bound A)) * (sin . (lower_bound A))) - ((cos . (upper_bound A)) * (sin . (upper_bound A)))) + (integral (cos (#) cos ),A)
A1:
[#] REAL is open Subset of REAL
;
A2:
((cos (#) cos ) || A) | A is bounded
by Lm20, INTEGRA5:9;
sin | A is continuous
;
then A3:
(- cos ) `| REAL is_integrable_on A
by Lm5, Th29, INTEGRA5:11;
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;
cos | A is continuous
;
then A5:
sin `| REAL is_integrable_on A
by Lm6, Th27, INTEGRA5:11;
cos (#) cos is_integrable_on A
by Lm20;
then A6:
(cos (#) cos ) || A is integrable
by INTEGRA5:def 2;
( ((- cos ) `| REAL ) | A is bounded & (sin `| REAL ) | A is bounded )
by Lm5, Lm6, Th27, Th29, INTEGRA5:10;
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 A3, A5, A1, 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 A6, A2, 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)
; verum