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