let th1, th2 be real number ; :: thesis: (cos (th1 + th2)) * (cos (th1 - th2)) = ((cos th2) * (cos th2)) - ((sin th1) * (sin th1))
(cos (th1 + th2)) * (cos (th1 - th2)) = ((cos th1) * (cos th1)) - ((sin th2) * (sin th2)) by Th45
.= (1 - ((sin th1) * (sin th1))) - ((sin th2) * (sin th2)) by Th7
.= (1 - ((sin th1) * (sin th1))) - (1 - ((cos th2) * (cos th2))) by Th6
.= ((cos th2) * (cos th2)) - ((sin th1) * (sin th1)) ;
hence (cos (th1 + th2)) * (cos (th1 - th2)) = ((cos th2) * (cos th2)) - ((sin th1) * (sin th1)) ; :: thesis: verum