theorem :: DIFF_2:66

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