let Z be open Subset of REAL ; :: thesis:
assume A1: Z c= ].(- 1),1.[ ; :: thesis:
A2: for x being Real st x in Z holds
arccot . x <> 0

proof

let x be Real; :: thesis:
assume A3: x in Z ; :: thesis:
assume A4: arccot . x = 0 ; :: thesis:
].(- 1),1.[ c= [.(- 1),1.] by XXREAL_1:25;
then Z c= [.(- 1),1.] by A1, XBOOLE_1:1;
then x in [.(- 1),1.] by A3;
then 0 in arccot .: [.(- 1),1.] by A4, SIN_COS9:24, FUNCT_1:def 12;
then A6: 0 in [.(PI / 4),((3 / 4) * PI ).] by SIN_COS9:56, RELAT_1:148;
PI in ].0 ,4.[ by SIN_COS:def 32;
then PI > 0 by XXREAL_1:4;
then PI / 4 > 0 / 4 by XREAL_1:76;
hence contradiction by A6, XXREAL_1:1; :: thesis:

end;

A7: arccot is_differentiable_on Z by A1, SIN_COS9:82;
then A8: arccot ^ is_differentiable_on Z by A2, FDIFF_2:22;
for x being Real st x in Z holds
((arccot ^ ) `| Z) . x = 1 / (((arccot . x) ^2 ) * (1 + (x ^2 )))

proof

let x be Real; :: thesis:
assume A9: x in Z ; :: thesis:
then A10: arccot . x <> 0 by A2;
A11: arccot is_differentiable_in x by A7, A9, FDIFF_1:16;
((arccot ^ ) `| Z) . x = diff (arccot ^ ),x by A8, A9, FDIFF_1:def 8
.= - ((diff arccot ,x) / ((arccot . x) ^2 )) by A10, A11, FDIFF_2:15
.= - (((arccot `| Z) . x) / ((arccot . x) ^2 )) by A7, A9, FDIFF_1:def 8
.= - ((- (1 / (1 + (x ^2 )))) / ((arccot . x) ^2 )) by A1, A9, SIN_COS9:82
.= (1 / (1 + (x ^2 ))) / ((arccot . x) ^2 )
.= 1 / (((arccot . x) ^2 ) * (1 + (x ^2 ))) by XCMPLX_1:79 ;
hence ((arccot ^ ) `| Z) . x = 1 / (((arccot . x) ^2 ) * (1 + (x ^2 ))) ; :: thesis:

end;

hence ( arccot ^ is_differentiable_on Z & ( for x being Real st x in Z holds
((arccot ^ ) `| Z) . x = 1 / (((arccot . x) ^2 ) * (1 + (x ^2 ))) ) ) by A2, A7, FDIFF_2:22; :: thesis: