let n be Element of NAT ; :: thesis:
let Z be open Subset of REAL ; :: thesis:
assume A1: ( Z c= dom ((#Z n) * arccot ) & Z c= ].(- 1),1.[ ) ; :: thesis:
then A2: Z c= dom (- ((#Z n) * arccot )) by VALUED_1:8;
A3: (#Z n) * arccot is_differentiable_on Z by A1, SIN_COS9:92;
then A4: (- 1) (#) ((#Z n) * arccot ) is_differentiable_on Z by A2, FDIFF_1:28, A;
for x being Real st x in Z holds
((- ((#Z n) * arccot )) `| Z) . x = (n * ((arccot . x) #Z (n - 1))) / (1 + (x ^2 ))

proof

let x be Real; :: thesis:
assume A5: x in Z ; :: thesis:
then A6: ( - 1 < x & x < 1 ) by A1, XXREAL_1:4;
arccot is_differentiable_on Z by A1, SIN_COS9:82;
then A8: arccot is_differentiable_in x by A5, FDIFF_1:16;
A9: (#Z n) * arccot is_differentiable_in x by A3, A5, FDIFF_1:16;
((- ((#Z n) * arccot )) `| Z) . x = diff (- ((#Z n) * arccot )),x by A4, A5, FDIFF_1:def 8
.= (- 1) * (diff ((#Z n) * arccot ),x) by A9, FDIFF_1:23, A
.= (- 1) * ((n * ((arccot . x) #Z (n - 1))) * (diff arccot ,x)) by A8, TAYLOR_1:3
.= (- 1) * ((n * ((arccot . x) #Z (n - 1))) * (- (1 / (1 + (x ^2 ))))) by A6, SIN_COS9:76
.= (n * ((arccot . x) #Z (n - 1))) / (1 + (x ^2 )) ;
hence ((- ((#Z n) * arccot )) `| Z) . x = (n * ((arccot . x) #Z (n - 1))) / (1 + (x ^2 )) ; :: thesis:

end;

hence ( - ((#Z n) * arccot ) is_differentiable_on Z & ( for x being Real st x in Z holds
((- ((#Z n) * arccot )) `| Z) . x = (n * ((arccot . x) #Z (n - 1))) / (1 + (x ^2 )) ) ) by A2, A3, FDIFF_1:28, A; :: thesis: