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