theorem :: DIFF_2:65

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