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:63, SIN_COS:64;
hence cot is_differentiable_in x by A4, FDIFF_2:14, SIN_COS:def 27; :: thesis: verum

end;

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

proof

let x be Element of 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 7;
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;
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 7, SIN_COS:def 27
.= - (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:102
.= (- 1) * ((1 * ((sin . x) ")) * (1 / (sin . x))) by XCMPLX_0:def 9
.= (- 1) * (((sin ^) . x) * (1 / (sin . x))) by A7, A9, RFUNCT_1:def 2
.= (- 1) * (((sin ^) . x) * (1 * ((sin . x) "))) by XCMPLX_0:def 9
.= (- 1) * (((sin ^) . x) * ((sin ^) . x)) by A7, A9, RFUNCT_1:def 2
.= (- 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:49 ;
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:61
.= (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 7;
hence ( cot is_differentiable_on Z & cot `| Z = ((- 1) (#) ((sin ^) ^2)) | Z ) by A2, A3, A13, A8, FDIFF_1:9, PARTFUN1:5; :: thesis: verum