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