let n be Element of NAT ; for A being non empty closed_interval Subset of REAL holds integral ((((#Z n) * cos) (#) sin),A) = (((- (1 / (n + 1))) (#) ((#Z (n + 1)) * cos)) . (upper_bound A)) - (((- (1 / (n + 1))) (#) ((#Z (n + 1)) * cos)) . (lower_bound A))
let A be non empty closed_interval Subset of REAL; integral ((((#Z n) * cos) (#) sin),A) = (((- (1 / (n + 1))) (#) ((#Z (n + 1)) * cos)) . (upper_bound A)) - (((- (1 / (n + 1))) (#) ((#Z (n + 1)) * cos)) . (lower_bound A))
A1:
[#] REAL = dom (((#Z n) * cos) (#) sin)
by FUNCT_2:def 1;
A2:
for x being Element of REAL st x in dom (((- (1 / (n + 1))) (#) ((#Z (n + 1)) * cos)) `| REAL) holds
(((- (1 / (n + 1))) (#) ((#Z (n + 1)) * cos)) `| REAL) . x = (((#Z n) * cos) (#) sin) . x
for x0 being Real holds (#Z n) * cos is_differentiable_in x0
then
( dom ((#Z n) * cos) = REAL & ( for x0 being Real st x0 in REAL holds
(#Z n) * cos is_differentiable_in x0 ) )
by FUNCT_2:def 1;
then
(#Z n) * cos is_differentiable_on REAL
by A1, FDIFF_1:9;
then A3:
(((#Z n) * cos) (#) sin) | REAL is continuous
by A1, FDIFF_1:21, FDIFF_1:25, SIN_COS:68;
then
(((#Z n) * cos) (#) sin) | A is continuous
by FCONT_1:16;
then A4:
((#Z n) * cos) (#) sin is_integrable_on A
by A1, INTEGRA5:11;
(- (1 / (n + 1))) (#) ((#Z (n + 1)) * cos) is_differentiable_on REAL
by Th4;
then
dom (((- (1 / (n + 1))) (#) ((#Z (n + 1)) * cos)) `| REAL) = dom (((#Z n) * cos) (#) sin)
by A1, FDIFF_1:def 7;
then A5:
((- (1 / (n + 1))) (#) ((#Z (n + 1)) * cos)) `| REAL = ((#Z n) * cos) (#) sin
by A2, PARTFUN1:5;
(((#Z n) * cos) (#) sin) | A is bounded
by A1, A3, INTEGRA5:10;
hence
integral ((((#Z n) * cos) (#) sin),A) = (((- (1 / (n + 1))) (#) ((#Z (n + 1)) * cos)) . (upper_bound A)) - (((- (1 / (n + 1))) (#) ((#Z (n + 1)) * cos)) . (lower_bound A))
by A4, A5, Th4, INTEGRA5:13; verum