theorem :: DIFF_3:57

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