theorem :: INTEGRA9:7

for n being 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))