theorem :: INTEGRA8:84

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))