theorem Th5: :: INTEGR11:5

for n, m being Element of NAT st m + n <> 0 & m - n <> 0 holds
( ((1 / (2 * (m + n))) (#) (sin * (AffineMap ((m + n),0)))) + ((1 / (2 * (m - n))) (#) (sin * (AffineMap ((m - n),0)))) is_differentiable_on REAL & ( for x being Real holds ((((1 / (2 * (m + n))) (#) (sin * (AffineMap ((m + n),0)))) + ((1 / (2 * (m - n))) (#) (sin * (AffineMap ((m - n),0))))) `| REAL) . x = (cos . (m * x)) * (cos . (n * x)) ) )