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