theorem :: DIFF_3:58

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