let Z be open Subset of REAL ; :: thesis: ( Z c= dom cot implies ( sin ^ is_differentiable_on Z & (sin ^ ) `| Z = (- ((sin ^ ) (#) cot )) | Z ) )
A1: dom cot = dom (cos (#) (sin ^ )) by RFUNCT_1:47, SIN_COS:def 31
.= (dom cos ) /\ (dom (sin ^ )) by VALUED_1:def 4 ;
assume A2: Z c= dom cot ; :: thesis: ( sin ^ is_differentiable_on Z & (sin ^ ) `| Z = (- ((sin ^ ) (#) cot )) | Z )
(dom cos ) /\ (dom (sin ^ )) c= dom (sin ^ ) by XBOOLE_1:17;
then A3: Z c= dom (sin ^ ) by A2, A1, XBOOLE_1:1;
A4: for x being Real st x in Z holds
sin . x <> 0 by A2, FDIFF_8:2;
then A5: sin ^ is_differentiable_on Z by FDIFF_4:40;
A6: for x being Real st x in dom ((sin ^ ) `| Z) holds
((sin ^ ) `| Z) . x = ((- ((sin ^ ) (#) cot )) | Z) . x

proof

let x be Real; :: thesis: ( x in dom ((sin ^ ) `| Z) implies ((sin ^ ) `| Z) . x = ((- ((sin ^ ) (#) cot )) | Z) . x )
A7: dom ((- 1) (#) ((sin ^ ) (#) cot )) = dom ((sin ^ ) (#) (cos / sin )) by SIN_COS:def 31, VALUED_1:def 5
.= dom ((sin ^ ) (#) (cos (#) (sin ^ ))) by RFUNCT_1:47 ;
A8: Z c= dom (cos (#) (sin ^ )) by A2, A1, VALUED_1:def 4;
dom ((sin ^ ) (#) (cos (#) (sin ^ ))) = (dom (sin ^ )) /\ (dom (cos (#) (sin ^ ))) by VALUED_1:def 4;
then A9: Z c= dom ((sin ^ ) (#) (cos (#) (sin ^ ))) by A3, A8, XBOOLE_1:19;
assume x in dom ((sin ^ ) `| Z) ; :: thesis: ((sin ^ ) `| Z) . x = ((- ((sin ^ ) (#) cot )) | Z) . x
then A10: x in Z by A5, FDIFF_1:def 8;
then ((sin ^ ) `| Z) . x = - ((cos . x) / ((sin . x) ^2 )) by A4, FDIFF_4:40
.= - ((1 * (cos . x)) / ((sin . x) * (sin . x)))
.= - ((1 / (sin . x)) * ((cos . x) / (sin . x))) by XCMPLX_1:77
.= - ((1 / (sin . x)) * ((cos . x) * (1 / (sin . x)))) by XCMPLX_1:100
.= - ((1 * ((sin . x) " )) * ((cos . x) * (1 / (sin . x)))) by XCMPLX_0:def 9
.= - (((sin . x) " ) * ((cos . x) * (1 * ((sin . x) " )))) by XCMPLX_0:def 9
.= - (((sin ^ ) . x) * ((cos . x) * ((sin . x) " ))) by A3, A10, RFUNCT_1:def 8
.= - (((sin ^ ) . x) * ((cos . x) * ((sin ^ ) . x))) by A3, A10, RFUNCT_1:def 8
.= - (((sin ^ ) . x) * ((cos (#) (sin ^ )) . x)) by A10, A8, VALUED_1:def 4
.= - (((sin ^ ) (#) (cos (#) (sin ^ ))) . x) by A10, A9, VALUED_1:def 4
.= - (((sin ^ ) (#) cot ) . x) by RFUNCT_1:47, SIN_COS:def 31
.= (- 1) * (((sin ^ ) (#) cot ) . x)
.= ((- 1) (#) ((sin ^ ) (#) cot )) . x by A10, A9, A7, VALUED_1:def 5
.= ((- ((sin ^ ) (#) cot )) | Z) . x by A10, FUNCT_1:72 ;
hence ((sin ^ ) `| Z) . x = ((- ((sin ^ ) (#) cot )) | Z) . x ; :: thesis: verum

end;

A11: dom ((- ((sin ^ ) (#) cot )) | Z) = (dom ((- 1) (#) ((sin ^ ) (#) cot ))) /\ Z by RELAT_1:90
.= (dom ((sin ^ ) (#) cot )) /\ Z by VALUED_1:def 5
.= ((dom (sin ^ )) /\ (dom cot )) /\ Z by VALUED_1:def 4
.= Z by A2, A3, XBOOLE_1:19, XBOOLE_1:28 ;
dom ((sin ^ ) `| Z) = Z by A5, FDIFF_1:def 8;
hence ( sin ^ is_differentiable_on Z & (sin ^ ) `| Z = (- ((sin ^ ) (#) cot )) | Z ) by A4, A11, A6, FDIFF_4:40, PARTFUN1:34; :: thesis: verum