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