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:13;
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