theorem :: DIFF_2:68

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