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