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