theorem :: DIFF_2:55

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