theorem :: INTEGRA8:75

for A being non empty closed_interval Subset of REAL
for x being Real
for n being Element of NAT st A = [.(x + ((2 * n) * PI)),(x + (((2 * n) + 1) * PI)).] holds
integral ((sin + cos),A) = (2 * (cos x)) - (2 * (sin x))