let Z be open Subset of REAL ; :: thesis: ( Z c= dom cot implies ( cot is_differentiable_on Z & cot `| Z = ((- 1) (#) ((sin ^ ) ^2 )) | Z ) )
assume A1: Z c= dom cot ; :: thesis: ( cot is_differentiable_on Z & cot `| Z = ((- 1) (#) ((sin ^ ) ^2 )) | Z )
A2: 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 A3: x in Z ; :: thesis: cot is_differentiable_in x
A4: sin is_differentiable_in x by SIN_COS:69;
A5: cos is_differentiable_in x by SIN_COS:68;
sin . x <> 0 by A1, A3, FDIFF_8:2;
hence cot is_differentiable_in x by A4, A5, FDIFF_2:14, SIN_COS:def 31; :: thesis: verum

end;

then A6: cot is_differentiable_on Z by A1, FDIFF_1:16;
then A7: dom (cot `| Z) = Z by FDIFF_1:def 8;
AA: dom cot = dom (cos (#) (sin ^ )) by RFUNCT_1:47, SIN_COS:def 31
.= (dom cos ) /\ (dom (sin ^ )) by VALUED_1:def 4 ;
AA1: (dom cos ) /\ (dom (sin ^ )) c= dom (sin ^ ) by XBOOLE_1:17;
then A9: Z c= dom (sin ^ ) by A1, AA, XBOOLE_1:1;
A10: 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 AA1, A1, AA, XBOOLE_1:1, XBOOLE_1:28 ;
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 A11: x in dom (cot `| Z) ; :: thesis: (cot `| Z) . x = (((- 1) (#) ((sin ^ ) (#) (sin ^ ))) | Z) . x
A: x in Z by A11, A6, FDIFF_1:def 8;
then A12: sin . x <> 0 by A1, FDIFF_8:2;
dom ((sin ^ ) (#) (sin ^ )) = (dom (sin ^ )) /\ (dom (sin ^ )) by VALUED_1:def 4
.= dom (sin ^ ) ;
then AA2: Z c= dom ((sin ^ ) (#) (sin ^ )) by A1, AA, AA1, XBOOLE_1:1;
then A14: x in dom ((sin ^ ) (#) (sin ^ )) by A;
A15: x in dom ((- 1) (#) ((sin ^ ) (#) (sin ^ ))) by A14, VALUED_1:def 5;
(cot `| Z) . x = diff (cos / sin ),x by A, A6, FDIFF_1:def 8, SIN_COS:def 31
.= - (1 / ((sin . x) ^2 )) by A12, 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 A, A9, RFUNCT_1:def 8
.= (- 1) * (((sin ^ ) . x) * (1 * ((sin . x) " ))) by XCMPLX_0:def 9
.= (- 1) * (((sin ^ ) . x) * ((sin ^ ) . x)) by A, A9, RFUNCT_1:def 8
.= (- 1) * (((sin ^ ) (#) (sin ^ )) . x) by AA2, A, VALUED_1:def 4
.= ((- 1) (#) ((sin ^ ) (#) (sin ^ ))) . x by A15, VALUED_1:def 5
.= (((- 1) (#) ((sin ^ ) (#) (sin ^ ))) | Z) . x by A, FUNCT_1:72 ;
hence (cot `| Z) . x = (((- 1) (#) ((sin ^ ) (#) (sin ^ ))) | Z) . x ; :: thesis: verum

end;

hence ( cot is_differentiable_on Z & cot `| Z = ((- 1) (#) ((sin ^ ) ^2 )) | Z ) by A7, A10, A1, A2, FDIFF_1:16, PARTFUN1:34; :: thesis: verum