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