theorem :: DIFF_2:63

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