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