theorem :: INTEGR11:32

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