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:116
.= (sin (th1 + th2)) / ((sin th1) * (sin th2)) by SIN_COS:75 ;
hence (cot th1) + (cot th2) = (sin (th1 + th2)) / ((sin th1) * (sin th2)) ; :: thesis: verum