theorem :: DIFF_2:49

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