theorem Th6: :: INTEGRA9:6

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