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