theorem Th19: :: INTEGR11:19

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