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