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

let x be Real; :: thesis:
assume A5: x in Z ; :: thesis:
A6: arccot is_differentiable_on Z by SIN_COS9:82, A1;
then A7: arccot is_differentiable_in x by A5, FDIFF_1:16;
A8: exp_R is_differentiable_in arccot . x by SIN_COS:70;
A9: exp_R * arccot is_differentiable_in x by A3, A5, FDIFF_1:16;
((- (exp_R * arccot )) `| Z) . x = diff (- (exp_R * arccot )),x by A4, A5, FDIFF_1:def 8
.= (- 1) * (diff (exp_R * arccot ),x) by A9, FDIFF_1:23, A
.= (- 1) * ((diff exp_R ,(arccot . x)) * (diff arccot ,x)) by A7, A8, FDIFF_2:13
.= (- 1) * ((diff exp_R ,(arccot . x)) * ((arccot `| Z) . x)) by A5, A6, FDIFF_1:def 8
.= (- 1) * ((diff exp_R ,(arccot . x)) * (- (1 / (1 + (x ^2 ))))) by A5, SIN_COS9:82, A1
.= (- 1) * (- ((diff exp_R ,(arccot . x)) * (1 / (1 + (x ^2 )))))
.= (exp_R . (arccot . x)) / (1 + (x ^2 )) by SIN_COS:70 ;
hence ((- (exp_R * arccot )) `| Z) . x = (exp_R . (arccot . x)) / (1 + (x ^2 )) ; :: thesis:

end;

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