theorem :: FDIFF_11:70

for n being Element of NAT
for Z being open Subset of REAL st Z c= dom ((1 / n) (#) ((#Z n) * (arccot ^))) & Z c= ].(- 1),1.[ & n > 0 holds
( (1 / n) (#) ((#Z n) * (arccot ^)) is_differentiable_on Z & ( for x being Real st x in Z holds
(((1 / n) (#) ((#Z n) * (arccot ^))) `| Z) . x = 1 / (((arccot . x) #Z (n + 1)) * (1 + (x ^2))) ) )