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