let x0, x1 be Real; :: thesis: [!sin,x0,x1!] = ((2 * (cos ((x0 + x1) / 2))) * (sin ((x0 - x1) / 2))) / (x0 - x1)
[!sin,x0,x1!] = ((sin x0) - (sin x1)) / (x0 - x1)
.= (2 * ((cos ((x0 + x1) / 2)) * (sin ((x0 - x1) / 2)))) / (x0 - x1) by SIN_COS4:16 ;
hence [!sin,x0,x1!] = ((2 * (cos ((x0 + x1) / 2))) * (sin ((x0 - x1) / 2))) / (x0 - x1) ; :: thesis: verum