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:29
.= (- ((1 / 2) * ((cos (2 * x)) - (cos 0)))) - (- ((1 / 2) * ((cos ((x - h) + (x - h))) - (cos ((x - h) - (x - h)))))) by SIN_COS4:29 ;
hence (bD ((sin (#) sin),h)) . x = (1 / 2) * ((cos (2 * (x - h))) - (cos (2 * x))) ; :: thesis: verum