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