let h, x be Real; :: thesis:
set y = 3 * x;
set z = 3 * h;
(cD (((sin (#) sin) (#) cos),h)) . x = (((sin (#) sin) (#) cos) . (x + (h / 2))) - (((sin (#) sin) (#) cos) . (x - (h / 2))) by DIFF_1:5
.= (((sin (#) sin) . (x + (h / 2))) * (cos . (x + (h / 2)))) - (((sin (#) sin) (#) cos) . (x - (h / 2))) by VALUED_1:5
.= (((sin . (x + (h / 2))) * (sin . (x + (h / 2)))) * (cos . (x + (h / 2)))) - (((sin (#) sin) (#) cos) . (x - (h / 2))) by VALUED_1:5
.= (((sin . (x + (h / 2))) * (sin . (x + (h / 2)))) * (cos . (x + (h / 2)))) - (((sin (#) sin) . (x - (h / 2))) * (cos . (x - (h / 2)))) by VALUED_1:5
.= (((sin (x + (h / 2))) * (sin (x + (h / 2)))) * (cos (x + (h / 2)))) - (((sin (x - (h / 2))) * (sin (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)))))) - (((sin (x - (h / 2))) * (sin (x - (h / 2)))) * (cos (x - (h / 2)))) by SIN_COS4:34
.= ((1 / 4) * ((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:34
.= ((1 / 4) * ((cos (x + (h / 2))) - (cos (x - (h / 2))))) - ((1 / 4) * ((cos (3 * (x + (h / 2)))) - (cos (3 * (x - (h / 2))))))
.= ((1 / 4) * (- (2 * ((sin (((x + (h / 2)) + (x - (h / 2))) / 2)) * (sin (((x + (h / 2)) - (x - (h / 2))) / 2)))))) - ((1 / 4) * ((cos (3 * (x + (h / 2)))) - (cos (3 * (x - (h / 2)))))) by SIN_COS4:18
.= ((1 / 4) * (- (2 * ((sin x) * (sin (h / 2)))))) - ((1 / 4) * (- (2 * ((sin ((((3 * x) + ((3 * h) / 2)) + ((3 * x) - ((3 * h) / 2))) / 2)) * (sin ((((3 * x) + ((3 * h) / 2)) - ((3 * x) - ((3 * h) / 2))) / 2)))))) by SIN_COS4:18
.= (- ((1 / 2) * ((sin x) * (sin (h / 2))))) + ((1 / 2) * ((sin (3 * x)) * (sin ((3 * h) / 2)))) ;
hence (cD (((sin (#) sin) (#) cos),h)) . x = (- ((1 / 2) * ((sin x) * (sin (h / 2))))) + ((1 / 2) * ((sin (3 * x)) * (sin ((3 * h) / 2)))) ; :: thesis: