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