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:31, SIN_COS:def 27
.= (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;
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 Element of REAL st x in dom ((sin ^) `| Z) holds
((sin ^) `| Z) . x = ((- ((sin ^) (#) cot)) | Z) . x

proof

let x be Element of 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 27, VALUED_1:def 5
.= dom ((sin ^) (#) (cos (#) (sin ^))) by RFUNCT_1:31 ;
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 7;
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:76
.= - ((1 / (sin . x)) * ((cos . x) * (1 / (sin . x)))) by XCMPLX_1:99
.= - ((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 2
.= - (((sin ^) . x) * ((cos . x) * ((sin ^) . x))) by A3, A10, RFUNCT_1:def 2
.= - (((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:31, SIN_COS:def 27
.= (- 1) * (((sin ^) (#) cot) . x)
.= ((- 1) (#) ((sin ^) (#) cot)) . x by A10, A9, A7, VALUED_1:def 5
.= ((- ((sin ^) (#) cot)) | Z) . x by A10, FUNCT_1:49 ;
hence ((sin ^) `| Z) . x = ((- ((sin ^) (#) cot)) | Z) . x ; :: thesis: verum

end;

A11: dom ((- ((sin ^) (#) cot)) | Z) = (dom ((- 1) (#) ((sin ^) (#) cot))) /\ Z by RELAT_1:61
.= (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 7;
hence ( sin ^ is_differentiable_on Z & (sin ^) `| Z = (- ((sin ^) (#) cot)) | Z ) by A4, A11, A6, FDIFF_4:40, PARTFUN1:5; :: thesis: verum