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