let x0, x1 be Real; :: thesis: [!(sin (#) cos),x0,x1!] = ((1 / 2) * ((sin (2 * x0)) - (sin (2 * x1)))) / (x0 - x1)
[!(sin (#) cos),x0,x1!] = (((sin . x0) * (cos . x0)) - ((sin (#) cos) . x1)) / (x0 - x1) by VALUED_1:5
.= (((sin x0) * (cos x0)) - ((sin x1) * (cos x1))) / (x0 - x1) by VALUED_1:5
.= (((1 / 2) * ((sin (x0 + x0)) + (sin (x0 - x0)))) - ((sin x1) * (cos x1))) / (x0 - x1) by SIN_COS4:30
.= (((1 / 2) * ((sin (x0 + x0)) + (sin (x0 - x0)))) - ((1 / 2) * ((sin (x1 + x1)) + (sin (x1 - x1))))) / (x0 - x1) by SIN_COS4:30
.= ((1 / 2) * ((sin (2 * x0)) - (sin (2 * x1)))) / (x0 - x1) ;
hence [!(sin (#) cos),x0,x1!] = ((1 / 2) * ((sin (2 * x0)) - (sin (2 * x1)))) / (x0 - x1) ; :: thesis: verum