let A be non empty 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:68, 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
;
( ((- 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:68
.=
(((- (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:12
.=
(((cos . (lower_bound A)) * (sin . (lower_bound A))) - ((cos . (upper_bound A)) * (sin . (upper_bound A)))) - (integral ((- 1) (#) ((cos (#) cos) || A)))
by RFUNCT_1:49
.=
(((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