let th1, th2 be Real; :: thesis: (sin (th1 + th2)) * (sin (th1 - th2)) = ((cos th2) * (cos th2)) - ((cos th1) * (cos th1))
(sin (th1 + th2)) * (sin (th1 - th2)) = ((sin th1) * (sin th1)) - ((sin th2) * (sin th2)) by Th37
.= (1 - ((cos th1) * (cos th1))) - ((sin th2) * (sin th2)) by Th4
.= (1 - (- (- ((cos th1) * (cos th1))))) - (- (- (1 - ((cos th2) * (cos th2))))) by Th4
.= ((cos th2) * (cos th2)) - ((cos th1) * (cos th1)) ;
hence (sin (th1 + th2)) * (sin (th1 - th2)) = ((cos th2) * (cos th2)) - ((cos th1) * (cos th1)) ; :: thesis: verum