theorem :: INTEGR11:20

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