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