theorem :: INTEGRA9:5

for n being Element of NAT
for A being non empty closed_interval Subset of REAL st n <> 0 holds
integral ((sin * (AffineMap (n,0))),A) = (((- (1 / n)) (#) (cos * (AffineMap (n,0)))) . (upper_bound A)) - (((- (1 / n)) (#) (cos * (AffineMap (n,0)))) . (lower_bound A))