let h, x be Real; (fD (sin,h)) . x = 2 * ((cos (((2 * x) + h) / 2)) * (sin (h / 2)))
(fD (sin,h)) . x =
(sin (x + h)) - (sin x)
by DIFF_1:3
.=
2 * ((cos ((x + (h + x)) / 2)) * (sin (((x + h) - x) / 2)))
by SIN_COS4:16
;
hence
(fD (sin,h)) . x = 2 * ((cos (((2 * x) + h) / 2)) * (sin (h / 2)))
; verum