let Z be open Subset of REAL ; :: thesis: ( Z c= dom cot implies ( cot is_differentiable_on Z & cot `| Z = ((- 1) (#) ((sin ^ ) ^2 )) | Z ) )
A1: (dom cos ) /\ (dom (sin ^ )) c= dom (sin ^ ) by XBOOLE_1:17;
assume A2: Z c= dom cot ; :: thesis: ( cot is_differentiable_on Z & cot `| Z = ((- 1) (#) ((sin ^ ) ^2 )) | Z )
A3: for x being Real st x in Z holds
cot is_differentiable_in x

proof

let x be Real; :: thesis: ( x in Z implies cot is_differentiable_in x )
assume x in Z ; :: thesis: cot is_differentiable_in x
then A4: sin . x <> 0 by A2, FDIFF_8:2;
( sin is_differentiable_in x & cos is_differentiable_in x ) by SIN_COS:68, SIN_COS:69;
hence cot is_differentiable_in x by A4, FDIFF_2:14, SIN_COS:def 31; :: thesis: verum

end;

then A5: cot is_differentiable_on Z by A2, FDIFF_1:16;
A6: dom cot = dom (cos (#) (sin ^ )) by RFUNCT_1:47, SIN_COS:def 31
.= (dom cos ) /\ (dom (sin ^ )) by VALUED_1:def 4 ;
then A7: Z c= dom (sin ^ ) by A2, A1, XBOOLE_1:1;
A8: for x being Real st x in dom (cot `| Z) holds
(cot `| Z) . x = (((- 1) (#) ((sin ^ ) (#) (sin ^ ))) | Z) . x

proof

let x be Real; :: thesis: ( x in dom (cot `| Z) implies (cot `| Z) . x = (((- 1) (#) ((sin ^ ) (#) (sin ^ ))) | Z) . x )
assume x in dom (cot `| Z) ; :: thesis: (cot `| Z) . x = (((- 1) (#) ((sin ^ ) (#) (sin ^ ))) | Z) . x
then A9: x in Z by A5, FDIFF_1:def 8;
then A10: sin . x <> 0 by A2, FDIFF_8:2;
dom ((sin ^ ) (#) (sin ^ )) = (dom (sin ^ )) /\ (dom (sin ^ )) by VALUED_1:def 4
.= dom (sin ^ ) ;
then A11: Z c= dom ((sin ^ ) (#) (sin ^ )) by A2, A6, A1, XBOOLE_1:1;
then x in dom ((sin ^ ) (#) (sin ^ )) by A9;
then A12: x in dom ((- 1) (#) ((sin ^ ) (#) (sin ^ ))) by VALUED_1:def 5;
(cot `| Z) . x = diff (cos / sin ),x by A5, A9, FDIFF_1:def 8, SIN_COS:def 31
.= - (1 / ((sin . x) ^2 )) by A10, FDIFF_7:47
.= (- 1) * (1 / ((sin . x) * (sin . x)))
.= (- 1) * ((1 / (sin . x)) * (1 / (sin . x))) by XCMPLX_1:103
.= (- 1) * ((1 * ((sin . x) " )) * (1 / (sin . x))) by XCMPLX_0:def 9
.= (- 1) * (((sin ^ ) . x) * (1 / (sin . x))) by A7, A9, RFUNCT_1:def 8
.= (- 1) * (((sin ^ ) . x) * (1 * ((sin . x) " ))) by XCMPLX_0:def 9
.= (- 1) * (((sin ^ ) . x) * ((sin ^ ) . x)) by A7, A9, RFUNCT_1:def 8
.= (- 1) * (((sin ^ ) (#) (sin ^ )) . x) by A9, A11, VALUED_1:def 4
.= ((- 1) (#) ((sin ^ ) (#) (sin ^ ))) . x by A12, VALUED_1:def 5
.= (((- 1) (#) ((sin ^ ) (#) (sin ^ ))) | Z) . x by A9, FUNCT_1:72 ;
hence (cot `| Z) . x = (((- 1) (#) ((sin ^ ) (#) (sin ^ ))) | Z) . x ; :: thesis: verum

end;

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