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