theorem :: DIFF_3:55

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