let h, x be Real; (fD (((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))))
(fD (((sin (#) sin) (#) sin),h)) . x =
(((sin (#) sin) (#) sin) . (x + h)) - (((sin (#) sin) (#) sin) . x)
by DIFF_1:3
.=
(((sin (#) sin) . (x + h)) * (sin . (x + h))) - (((sin (#) sin) (#) sin) . x)
by VALUED_1:5
.=
(((sin . (x + h)) * (sin . (x + h))) * (sin . (x + h))) - (((sin (#) sin) (#) sin) . x)
by VALUED_1:5
.=
(((sin . (x + h)) * (sin . (x + h))) * (sin . (x + h))) - (((sin (#) sin) . x) * (sin . x))
by VALUED_1:5
.=
(((sin (x + h)) * (sin (x + h))) * (sin (x + h))) - (((sin x) * (sin x)) * (sin x))
by VALUED_1:5
.=
((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))))) - (((sin x) * (sin x)) * (sin x))
by SIN_COS4:33
.=
((1 / 4) * ((((sin (x + h)) + (sin (x + h))) + (sin (x + h))) - (sin (3 * (x + h))))) - ((1 / 4) * ((((sin ((x + x) - x)) + (sin ((x + x) - x))) + (sin ((x + x) - x))) - (sin ((x + x) + x))))
by SIN_COS4:33
.=
(1 / 4) * ((3 * ((sin (x + h)) - (sin x))) - ((sin (3 * (x + h))) - (sin (3 * x))))
.=
(1 / 4) * ((3 * (2 * ((cos (((x + h) + x) / 2)) * (sin (((x + h) - x) / 2))))) - ((sin (3 * (x + h))) - (sin (3 * x))))
by SIN_COS4:16
.=
(1 / 4) * ((3 * (2 * ((cos (((x + h) + x) / 2)) * (sin (((x + h) - x) / 2))))) - (2 * ((cos (((3 * (x + h)) + (3 * x)) / 2)) * (sin (((3 * (x + h)) - (3 * x)) / 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
(fD (((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