theorem :: DIFF_2:52

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