let th be Real; :: thesis: ( cos th <> 0 implies sin th = (cos th) * (tan th) )
assume cos th <> 0 ; :: thesis: sin th = (cos th) * (tan th)
then sin th = ((cos th) / (cos th)) * (sin th) by XCMPLX_1:88
.= (cos th) * (tan th) by XCMPLX_1:75 ;
hence sin th = (cos th) * (tan th) ; :: thesis: verum