let th1, th2 be Real; :: thesis: (cos (th1 + th2)) * (cos (th1 - th2)) = ((cos th1) * (cos th1)) - ((sin th2) * (sin 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)))) * (((cos th1) * (cos th2)) + ((sin th1) * (sin th2))) by SIN_COS:83
.= (((((cos th1) * (cos th1)) * ((cos th2) * (cos th2))) + (((cos th1) * (cos th2)) * ((sin th1) * (sin th2)))) + (- (((sin th1) * (sin th2)) * ((cos th1) * (cos th2))))) + (- ((((sin th1) * (sin th1)) * (sin th2)) * (sin th2)))
.= (((cos th1) * (cos th1)) * (1 - (- (- ((sin th2) * (sin th2)))))) + (- (((sin th1) * (sin th1)) * ((sin th2) * (sin th2)))) by Th5
.= (((cos th1) * (cos th1)) * 1) + (((sin th2) * (sin th2)) * (- (((cos th1) * (cos th1)) + ((sin th1) * (sin th1)))))
.= (((cos th1) * (cos th1)) * 1) + (((sin th2) * (sin th2)) * (- 1)) by SIN_COS:29
.= ((cos th1) * (cos th1)) - ((sin th2) * (sin th2)) ;
hence (cos (th1 + th2)) * (cos (th1 - th2)) = ((cos th1) * (cos th1)) - ((sin th2) * (sin th2)) ; :: thesis: verum