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