theorem :: SIN_COS9:116

for Z being open Subset of REAL st Z c= dom (arccot * exp_R) & ( for x being Real st x in Z holds
exp_R . x < 1 ) holds
( arccot * exp_R is_differentiable_on Z & ( for x being Real st x in Z holds
((arccot * exp_R) `| Z) . x = - ((exp_R . x) / (1 + ((exp_R . x) ^2))) ) )