theorem :: DIFF_2:51

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