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