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