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