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 A1: 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 ) ) )
AA: Z c= dom cosec by A1, VALUED_1:8;
then A2: for x being Real st x in Z holds
sin . x <> 0 by RFUNCT_1:13;
A3: sin is_differentiable_on Z by FDIFF_1:34, SIN_COS:73;
then A4: cosec is_differentiable_on Z by A2, FDIFF_2:22;
then A6: (- 1) (#) cosec is_differentiable_on Z by A1, FDIFF_1:28;
for x being Real st x in Z holds
((- cosec ) `| Z) . x = (cos . x) / ((sin . x) ^2 )

proof

let x be Real; :: thesis: ( x in Z implies ((- cosec ) `| Z) . x = (cos . x) / ((sin . x) ^2 ) )
assume A7: x in Z ; :: thesis: ((- cosec ) `| Z) . x = (cos . x) / ((sin . x) ^2 )
then A8: sin . x <> 0 by AA, RFUNCT_1:13;
A9: sin is_differentiable_in x by A3, A7, FDIFF_1:16;
((- cosec ) `| Z) . x = (- 1) * (diff (sin ^ ),x) by A1, A4, A7, FDIFF_1:28
.= (- 1) * (- ((diff sin ,x) / ((sin . x) ^2 ))) by A8, A9, FDIFF_2:15
.= (cos . x) / ((sin . x) ^2 ) by SIN_COS:69 ;
hence ((- cosec ) `| Z) . x = (cos . x) / ((sin . x) ^2 ) ; :: thesis: verum

end;

hence ( - cosec is_differentiable_on Z & ( for x being Real st x in Z holds
((- cosec ) `| Z) . x = (cos . x) / ((sin . x) ^2 ) ) ) by A6; :: thesis: verum