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)) ) ) )
A1: sin is_differentiable_on Z by FDIFF_1:26, SIN_COS:68;
assume A2: 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)) ) )
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 & sin is_differentiable_in x ) by A2, A1, FDIFF_1:9;
((sin ^) `| Z) . x = diff ((sin ^),x) by A3, A4, FDIFF_1:def 7
.= - ((diff (sin,x)) / ((sin . x) ^2)) by A5, FDIFF_2:15
.= - ((cos . x) / ((sin . x) ^2)) by SIN_COS:64 ;
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 A2, A1, FDIFF_2:22; :: thesis: verum