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