let h, x be Real; :: thesis: (cD ((sin (#) cos),h)) . x = (1 / 2) * ((sin ((2 * x) + h)) - (sin ((2 * x) - h)))
(cD ((sin (#) cos),h)) . x = ((sin (#) cos) . (x + (h / 2))) - ((sin (#) cos) . (x - (h / 2))) by DIFF_1:5
.= ((sin . (x + (h / 2))) * (cos . (x + (h / 2)))) - ((sin (#) cos) . (x - (h / 2))) by VALUED_1:5
.= ((sin (x + (h / 2))) * (cos (x + (h / 2)))) - ((sin (x - (h / 2))) * (cos (x - (h / 2)))) by VALUED_1:5
.= ((1 / 2) * ((sin ((x + (h / 2)) + (x + (h / 2)))) + (sin ((x + (h / 2)) - (x + (h / 2)))))) - ((sin (x - (h / 2))) * (cos (x - (h / 2)))) by SIN_COS4:30
.= ((1 / 2) * ((sin ((x + (h / 2)) + (x + (h / 2)))) + (sin ((x + (h / 2)) - (x + (h / 2)))))) - ((1 / 2) * ((sin ((x - (h / 2)) + (x - (h / 2)))) + (sin ((x - (h / 2)) - (x - (h / 2)))))) by SIN_COS4:30
.= ((1 / 2) * (sin (2 * (x + (h / 2))))) - ((1 / 2) * (sin (2 * (x - (h / 2))))) ;
hence (cD ((sin (#) cos),h)) . x = (1 / 2) * ((sin ((2 * x) + h)) - (sin ((2 * x) - h))) ; :: thesis: verum