let th1, th2 be Real; :: thesis: ( sin th1 <> 0 & sin th2 <> 0 implies (cot th1) - (cot th2) = - ((sin (th1 - th2)) / ((sin th1) * (sin th2))) )
assume ( sin th1 <> 0 & sin th2 <> 0 ) ; :: thesis: (cot th1) - (cot th2) = - ((sin (th1 - th2)) / ((sin th1) * (sin th2)))
then (cot th1) - (cot th2) = (((cos th1) * (sin th2)) - (- (- ((cos th2) * (sin th1))))) / ((sin th1) * (sin th2)) by XCMPLX_1:130
.= (- (((sin th1) * (cos th2)) - ((cos th1) * (sin th2)))) / ((sin th1) * (sin th2))
.= (- (sin (th1 - th2))) / ((sin th1) * (sin th2)) by SIN_COS:82
.= - ((sin (th1 - th2)) / ((sin th1) * (sin th2))) by XCMPLX_1:187 ;
hence (cot th1) - (cot th2) = - ((sin (th1 - th2)) / ((sin th1) * (sin th2))) ; :: thesis: verum