let Z be open Subset of REAL ; :: thesis: ( Z c= dom cot implies ( sin ^ is_differentiable_on Z & (sin ^ ) `| Z = (- ((sin ^ ) (#) cot )) | Z ) )
assume A1: Z c= dom cot ; :: thesis: ( sin ^ is_differentiable_on Z & (sin ^ ) `| Z = (- ((sin ^ ) (#) cot )) | Z )
A2: for x being Real st x in Z holds
sin . x <> 0 by A1, FDIFF_8:2;
then A4: sin ^ is_differentiable_on Z by FDIFF_4:40;
then A5: dom ((sin ^ ) `| Z) = Z by FDIFF_1:def 8;
A7: dom cot = dom (cos (#) (sin ^ )) by RFUNCT_1:47, SIN_COS:def 31
.= (dom cos ) /\ (dom (sin ^ )) by VALUED_1:def 4 ;
(dom cos ) /\ (dom (sin ^ )) c= dom (sin ^ ) by XBOOLE_1:17;
then A9: Z c= dom (sin ^ ) by A7, A1, XBOOLE_1:1;
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 A9, A1, XBOOLE_1:19, XBOOLE_1:28 ;
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 )
assume B1: x in dom ((sin ^ ) `| Z) ; :: thesis: ((sin ^ ) `| Z) . x = ((- ((sin ^ ) (#) cot )) | Z) . x
A12: x in Z by B1, A4, FDIFF_1:def 8;
A14: Z c= dom (cos (#) (sin ^ )) by A1, A7, VALUED_1:def 4;
dom ((sin ^ ) (#) (cos (#) (sin ^ ))) = (dom (sin ^ )) /\ (dom (cos (#) (sin ^ ))) by VALUED_1:def 4;
then A16: Z c= dom ((sin ^ ) (#) (cos (#) (sin ^ ))) by A14, A9, XBOOLE_1:19;
AAA: 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 ;
((sin ^ ) `| Z) . x = - ((cos . x) / ((sin . x) ^2 )) by A2, A12, 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 A9, A12, RFUNCT_1:def 8
.= - (((sin ^ ) . x) * ((cos . x) * ((sin ^ ) . x))) by A9, A12, RFUNCT_1:def 8
.= - (((sin ^ ) . x) * ((cos (#) (sin ^ )) . x)) by A12, A14, VALUED_1:def 4
.= - (((sin ^ ) (#) (cos (#) (sin ^ ))) . x) by A16, A12, VALUED_1:def 4
.= - (((sin ^ ) (#) cot ) . x) by RFUNCT_1:47, SIN_COS:def 31
.= (- 1) * (((sin ^ ) (#) cot ) . x)
.= ((- 1) (#) ((sin ^ ) (#) cot )) . x by A16, A12, AAA, VALUED_1:def 5
.= ((- ((sin ^ ) (#) cot )) | Z) . x by A12, FUNCT_1:72 ;
hence ((sin ^ ) `| Z) . x = ((- ((sin ^ ) (#) cot )) | Z) . x ; :: thesis: verum

end;

hence ( sin ^ is_differentiable_on Z & (sin ^ ) `| Z = (- ((sin ^ ) (#) cot )) | Z ) by A2, A5, A11, FDIFF_4:40, PARTFUN1:34; :: thesis: verum