theorem :: DIFF_3:60

for h, x being Real holds (cD (((cos (#) cos) (#) cos),h)) . x = - ((1 / 2) * (((3 * (sin x)) * (sin (h / 2))) + ((sin (3 * x)) * (sin ((3 * h) / 2)))))