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