theorem :: SIN_COS9:115

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