let th1, th2 be Real; :: thesis: (sin (th1 + th2)) - (sin (th1 - th2)) = 2 * ((cos th1) * (sin 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 * ((cos th1) * (sin th2)) ;
hence (sin (th1 + th2)) - (sin (th1 - th2)) = 2 * ((cos th1) * (sin th2)) ; :: thesis: verum