let x be real number ; :: thesis: ( sin x <> 0 implies cos x = (sin x) * (cot x) )
assume sin x <> 0 ; :: thesis: cos x = (sin x) * (cot x)
then cos x = ((sin x) / (sin x)) * (cos x) by XCMPLX_1:89
.= (sin x) * (cot x) by XCMPLX_1:76 ;
hence cos x = (sin x) * (cot x) ; :: thesis: verum