let Z be open Subset of REAL; :: thesis: ( Z c= dom (arctan * ln) & ( for x being Real st x in Z holds
( ln . x > - 1 & ln . x < 1 ) ) implies ( arctan * ln is_differentiable_on Z & ( for x being Real st x in Z holds
((arctan * ln) `| Z) . x = 1 / (x * (1 + ((ln . x) ^2))) ) ) )
A1: right_open_halfline 0 = { g where g is Real : 0 < g } by XXREAL_1:230;
assume that
A2: Z c= dom (arctan * ln) and
A3: for x being Real st x in Z holds
( ln . x > - 1 & ln . x < 1 ) ; :: thesis: ( arctan * ln is_differentiable_on Z & ( for x being Real st x in Z holds
((arctan * ln) `| Z) . x = 1 / (x * (1 + ((ln . x) ^2))) ) )
dom (arctan * ln) c= dom ln by RELAT_1:25;
then A4: Z c= dom ln by A2;
A5: for x being Real st x in Z holds
x > 0

proof

let x be Real; :: thesis: ( x in Z implies x > 0 )
assume x in Z ; :: thesis: x > 0
then x in right_open_halfline 0 by A4, TAYLOR_1:18;
then ex g being Real st
( x = g & 0 < g ) by A1;
hence x > 0 ; :: thesis: verum

end;

A6: for x being Real st x in Z holds
arctan * ln is_differentiable_in x

proof

let x be Real; :: thesis: ( x in Z implies arctan * ln is_differentiable_in x )
assume A7: x in Z ; :: thesis: arctan * ln is_differentiable_in x
then A8: ln . x > - 1 by A3;
A9: ln . x < 1 by A3, A7;
ln is_differentiable_in x by A5, A7, TAYLOR_1:18;
hence arctan * ln is_differentiable_in x by A8, A9, Th85; :: thesis: verum

end;

then A10: arctan * ln is_differentiable_on Z by A2, FDIFF_1:9;
for x being Real st x in Z holds
((arctan * ln) `| Z) . x = 1 / (x * (1 + ((ln . x) ^2)))

proof

let x be Real; :: thesis: ( x in Z implies ((arctan * ln) `| Z) . x = 1 / (x * (1 + ((ln . x) ^2))) )
assume A11: x in Z ; :: thesis: ((arctan * ln) `| Z) . x = 1 / (x * (1 + ((ln . x) ^2)))
then A12: ln is_differentiable_in x by A5, TAYLOR_1:18;
A13: ln . x < 1 by A3, A11;
A14: ln . x > - 1 by A3, A11;
x > 0 by A5, A11;
then A15: x in right_open_halfline 0 by A1;
((arctan * ln) `| Z) . x = diff ((arctan * ln),x) by A10, A11, FDIFF_1:def 7
.= (diff (ln,x)) / (1 + ((ln . x) ^2)) by A12, A14, A13, Th85
.= (1 / x) / (1 + ((ln . x) ^2)) by A15, TAYLOR_1:18
.= 1 / (x * (1 + ((ln . x) ^2))) by XCMPLX_1:78 ;
hence ((arctan * ln) `| Z) . x = 1 / (x * (1 + ((ln . x) ^2))) ; :: thesis: verum

end;

hence ( arctan * ln is_differentiable_on Z & ( for x being Real st x in Z holds
((arctan * ln) `| Z) . x = 1 / (x * (1 + ((ln . x) ^2))) ) ) by A2, A6, FDIFF_1:9; :: thesis: verum