theorem :: DIFF_2:53

for x0, x1 being Real holds [!(sin (#) cos),x0,x1!] = ((1 / 2) * ((sin (2 * x0)) - (sin (2 * x1)))) / (x0 - x1)