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