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