let n be Element of NAT ; for A being non empty closed_interval Subset of REAL st n <> 0 holds
integral ((cos * (AffineMap (n,0))),A) = (((1 / n) (#) (sin * (AffineMap (n,0)))) . (upper_bound A)) - (((1 / n) (#) (sin * (AffineMap (n,0)))) . (lower_bound A))
let A be non empty closed_interval Subset of REAL; ( n <> 0 implies integral ((cos * (AffineMap (n,0))),A) = (((1 / n) (#) (sin * (AffineMap (n,0)))) . (upper_bound A)) - (((1 / n) (#) (sin * (AffineMap (n,0)))) . (lower_bound A)) )
assume A1:
n <> 0
; integral ((cos * (AffineMap (n,0))),A) = (((1 / n) (#) (sin * (AffineMap (n,0)))) . (upper_bound A)) - (((1 / n) (#) (sin * (AffineMap (n,0)))) . (lower_bound A))
A2:
[#] REAL = dom (cos * (AffineMap (n,0)))
by FUNCT_2:def 1;
A3:
for x being Real st x in REAL holds
(AffineMap (n,0)) . x = n * x
A4:
for x being Element of REAL st x in dom (((1 / n) (#) (sin * (AffineMap (n,0)))) `| REAL) holds
(((1 / n) (#) (sin * (AffineMap (n,0)))) `| REAL) . x = (cos * (AffineMap (n,0))) . x
proof
let x be
Element of
REAL ;
( x in dom (((1 / n) (#) (sin * (AffineMap (n,0)))) `| REAL) implies (((1 / n) (#) (sin * (AffineMap (n,0)))) `| REAL) . x = (cos * (AffineMap (n,0))) . x )
assume
x in dom (((1 / n) (#) (sin * (AffineMap (n,0)))) `| REAL)
;
(((1 / n) (#) (sin * (AffineMap (n,0)))) `| REAL) . x = (cos * (AffineMap (n,0))) . x
(((1 / n) (#) (sin * (AffineMap (n,0)))) `| REAL) . x =
cos (n * x)
by A1, Th6
.=
cos . ((AffineMap (n,0)) . x)
by A3
.=
(cos * (AffineMap (n,0))) . x
by A2, FUNCT_1:12
;
hence
(((1 / n) (#) (sin * (AffineMap (n,0)))) `| REAL) . x = (cos * (AffineMap (n,0))) . x
;
verum
end;
(1 / n) (#) (sin * (AffineMap (n,0))) is_differentiable_on REAL
by A1, Th6;
then
dom (((1 / n) (#) (sin * (AffineMap (n,0)))) `| REAL) = dom (cos * (AffineMap (n,0)))
by A2, FDIFF_1:def 7;
then A5:
((1 / n) (#) (sin * (AffineMap (n,0)))) `| REAL = cos * (AffineMap (n,0))
by A4, PARTFUN1:5;
(cos * (AffineMap (n,0))) | A is continuous
;
then A6:
cos * (AffineMap (n,0)) is_integrable_on A
by A2, INTEGRA5:11;
(cos * (AffineMap (n,0))) | A is bounded
by A2, INTEGRA5:10;
hence
integral ((cos * (AffineMap (n,0))),A) = (((1 / n) (#) (sin * (AffineMap (n,0)))) . (upper_bound A)) - (((1 / n) (#) (sin * (AffineMap (n,0)))) . (lower_bound A))
by A1, A6, A5, Th6, INTEGRA5:13; verum