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