let x be Real; :: thesis: ( cos x <> 0 implies cosec x = (sec x) / (tan x) )
assume A1: cos x <> 0 ; :: thesis: cosec x = (sec x) / (tan x)
then (sec x) / (tan x) = ((1 / (cos x)) * (cos x)) / (((sin x) / (cos x)) * (cos x)) by XCMPLX_1:91
.= 1 / (((sin x) / (cos x)) * (cos x)) by A1, XCMPLX_1:87
.= 1 / (sin x) by A1, XCMPLX_1:87 ;
hence cosec x = (sec x) / (tan x) ; :: thesis: verum