theorem :: DIFF_3:59

for h, x being Real holds (bD (((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)))))