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:75
.= 2 * ((cos ((th1 / 2) - (th2 / 2))) * (sin ((th1 + th2) / 2))) by SIN_COS:83
.= 2 * ((cos ((th1 - th2) / 2)) * (sin ((th1 + th2) / 2))) ;
hence (sin th1) + (sin th2) = 2 * ((cos ((th1 - th2) / 2)) * (sin ((th1 + th2) / 2))) ; :: thesis: