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