theorem :: SIN_COS9:114

for r, s, h being Real
for Z being open Subset of REAL
for f, f1, f2 being PartFunc of REAL,REAL st Z c= dom (arccot * f) & f = f1 + (h (#) f2) & ( for x being Real st x in Z holds
( f . x > - 1 & f . x < 1 ) ) & ( for x being Real st x in Z holds
f1 . x = r + (s * x) ) & f2 = #Z 2 holds
( arccot * (f1 + (h (#) f2)) is_differentiable_on Z & ( for x being Real st x in Z holds
((arccot * (f1 + (h (#) f2))) `| Z) . x = - ((s + ((2 * h) * x)) / (1 + (((r + (s * x)) + (h * (x ^2))) ^2))) ) )