theorem :: INTEGR11:28

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