let x0, x1 be Real; :: thesis: [!((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))
[!((cos (#) cos) (#) cos),x0,x1!] = ((((cos (#) cos) . x0) * (cos . x0)) - (((cos (#) cos) (#) cos) . x1)) / (x0 - x1) by VALUED_1:5
.= ((((cos . x0) * (cos . x0)) * (cos . x0)) - (((cos (#) cos) (#) cos) . x1)) / (x0 - x1) by VALUED_1:5
.= ((((cos . x0) * (cos . x0)) * (cos . x0)) - (((cos (#) cos) . x1) * (cos . x1))) / (x0 - x1) by VALUED_1:5
.= ((((cos x0) * (cos x0)) * (cos x0)) - (((cos x1) * (cos x1)) * (cos x1))) / (x0 - x1) by VALUED_1:5
.= (((1 / 4) * ((((cos ((x0 + x0) - x0)) + (cos ((x0 + x0) - x0))) + (cos ((x0 + x0) - x0))) + (cos ((x0 + x0) + x0)))) - (((cos x1) * (cos x1)) * (cos x1))) / (x0 - x1) by SIN_COS4:36
.= (((1 / 4) * ((((cos x0) + (cos x0)) + (cos x0)) + (cos (3 * x0)))) - ((1 / 4) * ((((cos ((x1 + x1) - x1)) + (cos ((x1 + x1) - x1))) + (cos ((x1 + x1) - x1))) + (cos ((x1 + x1) + x1))))) / (x0 - x1) by SIN_COS4:36
.= ((1 / 4) * ((3 * ((cos x0) - (cos x1))) + ((cos (3 * x0)) - (cos (3 * x1))))) / (x0 - x1)
.= ((1 / 4) * ((3 * (- (2 * ((sin ((x0 + x1) / 2)) * (sin ((x0 - x1) / 2)))))) + ((cos (3 * x0)) - (cos (3 * x1))))) / (x0 - x1) by SIN_COS4:18
.= ((1 / 4) * (((3 * (- 2)) * ((sin ((x0 + x1) / 2)) * (sin ((x0 - x1) / 2)))) + (- (2 * ((sin (((3 * x0) + (3 * x1)) / 2)) * (sin (((3 * x0) - (3 * x1)) / 2))))))) / (x0 - x1) by SIN_COS4:18
.= (- ((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) ;
hence [!((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)) ; :: thesis: verum