theorem Th22: :: INTEGR11:22

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