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:34
.= ((1 / 2) * ((sin (x + x)) + (sin 0 ))) - ((1 / 2) * ((sin ((x - h) + (x - h))) + (sin ((x - h) - (x - h))))) by SIN_COS4:34
.= ((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