let th1, th2 be Real; :: thesis:
(sin th1) - (sin th2) = (sin ((th1 / 2) + (th1 / 2))) - (sin ((th2 / 2) + (th2 / 2)))
.= (((sin (th1 / 2)) * (cos (th1 / 2))) + ((cos (th1 / 2)) * (sin (th1 / 2)))) - (sin ((th2 / 2) + (th2 / 2))) by SIN_COS:75
.= (2 * ((sin (th1 / 2)) * (cos (th1 / 2)))) - (((sin (th2 / 2)) * (cos (th2 / 2))) + ((sin (th2 / 2)) * (cos (th2 / 2)))) by SIN_COS:75
.= 2 * ((((sin (th1 / 2)) * (cos (th1 / 2))) * 1) - ((sin (th2 / 2)) * (cos (th2 / 2))))
.= 2 * ((((sin (th1 / 2)) * (cos (th1 / 2))) * (((cos (th2 / 2)) * (cos (th2 / 2))) + ((sin (th2 / 2)) * (sin (th2 / 2))))) - (((sin (th2 / 2)) * (cos (th2 / 2))) * 1)) by SIN_COS:29
.= 2 * (((((sin (th1 / 2)) * (cos (th1 / 2))) * ((cos (th2 / 2)) * (cos (th2 / 2)))) + (((sin (th1 / 2)) * (cos (th1 / 2))) * ((sin (th2 / 2)) * (sin (th2 / 2))))) - (((sin (th2 / 2)) * (cos (th2 / 2))) * (((cos (th1 / 2)) * (cos (th1 / 2))) + ((sin (th1 / 2)) * (sin (th1 / 2)))))) by SIN_COS:29
.= 2 * ((((sin (th1 / 2)) * (cos (th2 / 2))) - ((cos (th1 / 2)) * (sin (th2 / 2)))) * (((cos (th1 / 2)) * (cos (th2 / 2))) + (- ((sin (th1 / 2)) * (sin (th2 / 2))))))
.= 2 * ((sin ((th1 / 2) - (th2 / 2))) * (((cos (th1 / 2)) * (cos (th2 / 2))) - ((sin (th1 / 2)) * (sin (th2 / 2))))) by SIN_COS:82
.= 2 * ((sin ((th1 - th2) / 2)) * (cos ((th1 / 2) + (th2 / 2)))) by SIN_COS:75
.= 2 * ((cos ((th1 + th2) / 2)) * (sin ((th1 - th2) / 2))) ;
hence (sin th1) - (sin th2) = 2 * ((cos ((th1 + th2) / 2)) * (sin ((th1 - th2) / 2))) ; :: thesis: