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