let Z be open Subset of REAL ; :: thesis: ( ( for x being Real st x in Z holds
sin . x <> 0 ) implies ( sin ^ is_differentiable_on Z & ( for x being Real st x in Z holds
((sin ^ ) `| Z) . x = - ((cos . x) / ((sin . x) ^2 )) ) ) )
assume A1: for x being Real st x in Z holds
sin . x <> 0 ; :: thesis: ( sin ^ is_differentiable_on Z & ( for x being Real st x in Z holds
((sin ^ ) `| Z) . x = - ((cos . x) / ((sin . x) ^2 )) ) )
A2: sin is_differentiable_on Z by FDIFF_1:34, SIN_COS:73;
then A3: sin ^ is_differentiable_on Z by A1, FDIFF_2:22;
for x being Real st x in Z holds
((sin ^ ) `| Z) . x = - ((cos . x) / ((sin . x) ^2 ))

proof

let x be Real; :: thesis: ( x in Z implies ((sin ^ ) `| Z) . x = - ((cos . x) / ((sin . x) ^2 )) )
assume A4: x in Z ; :: thesis: ((sin ^ ) `| Z) . x = - ((cos . x) / ((sin . x) ^2 ))
then A5: sin . x <> 0 by A1;
A6: sin is_differentiable_in x by A2, A4, FDIFF_1:16;
((sin ^ ) `| Z) . x = diff (sin ^ ),x by A3, A4, FDIFF_1:def 8
.= - ((diff sin ,x) / ((sin . x) ^2 )) by A5, A6, FDIFF_2:15
.= - ((cos . x) / ((sin . x) ^2 )) by SIN_COS:69 ;
hence ((sin ^ ) `| Z) . x = - ((cos . x) / ((sin . x) ^2 )) ; :: thesis: verum

end;

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