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