theorem :: DIFF_2:56

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