let Z be open Subset of REAL; :: thesis: ( Z c= dom cosec implies ( cosec is_differentiable_on Z & ( for x being Real st x in Z holds
(cosec `| Z) . x = - ((cos . x) / ((sin . x) ^2)) ) ) )
assume Z c= dom cosec ; :: thesis: ( cosec is_differentiable_on Z & ( for x being Real st x in Z holds
(cosec `| Z) . x = - ((cos . x) / ((sin . x) ^2)) ) )
then for x being Real st x in Z holds
sin . x <> 0 by RFUNCT_1:3;
hence ( cosec is_differentiable_on Z & ( for x being Real st x in Z holds
(cosec `| Z) . x = - ((cos . x) / ((sin . x) ^2)) ) ) by FDIFF_4:40; :: thesis: verum