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:69;
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:69 ;
hence ( cosec is_differentiable_in x & diff cosec ,x = - ((cos . x) / ((sin . x) ^2 )) ) by A2, A1, FDIFF_2:15; :: thesis: verum