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