theorem :: INTEGR11:24

for n being Element of NAT
for A being non empty closed_interval Subset of REAL st A = [.(- (PI / 2)),(PI / 2).] holds
integral ((((#Z n) * cos) (#) sin),A) = 0