let x be Real; :: thesis: ( sin . x <> 0 implies ( cosec is_differentiable_in x & diff (cosec,x) = - ((cos . x) / ((sin . x) ^2)) ) )
A1: sin is_differentiable_in x by SIN_COS:64;
assume A2: sin . x <> 0 ; :: thesis: ( cosec is_differentiable_in x & diff (cosec,x) = - ((cos . x) / ((sin . x) ^2)) )
then diff ((sin ^),x) = - ((diff (sin,x)) / ((sin . x) ^2)) by A1, FDIFF_2:15
.= - ((cos . x) / ((sin . x) ^2)) by SIN_COS:64 ;
hence ( cosec is_differentiable_in x & diff (cosec,x) = - ((cos . x) / ((sin . x) ^2)) ) by A2, A1, FDIFF_2:15; :: thesis: verum