theorem :: DIFF_3:56

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