let th1, th2 be Real; :: 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 Th41
.= (1 - ((sin th1) * (sin th1))) - ((sin th2) * (sin th2)) by Th5
.= (1 - ((sin th1) * (sin th1))) - (1 - ((cos th2) * (cos th2))) by Th4
.= ((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