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