let Z be open Subset of REAL ; :: thesis:
assume A1: Z c= ].(- 1),1.[ ; :: thesis:
A2: Z c= dom (id Z) by FUNCT_1:34;
].(- 1),1.[ c= [.(- 1),1.] by XXREAL_1:25;
then ].(- 1),1.[ c= dom arctan by Th21, XBOOLE_1:1;
then Z c= dom arctan by A1, XBOOLE_1:1;
then Z c= (dom (id Z)) /\ (dom arctan ) by A2, XBOOLE_1:19;
then A3: Z c= dom ((id Z) (#) arctan ) by VALUED_1:def 4;
A4: for x being Real st x in Z holds
(id Z) . x = (1 * x) + 0 by FUNCT_1:35;
then A5: ( id Z is_differentiable_on Z & ( for x being Real st x in Z holds
((id Z) `| Z) . x = 1 ) ) by A2, FDIFF_1:31;
A6: arctan is_differentiable_on Z by A1, Th79;
for x being Real st x in Z holds
(((id Z) (#) arctan ) `| Z) . x = (arctan . x) + (x / (1 + (x ^2 )))

let x be Real; :: thesis:
assume A7: x in Z ; :: thesis:
then A8: ( - 1 < x & x < 1 ) by A1, XXREAL_1:4;
(((id Z) (#) arctan ) `| Z) . x = ((arctan . x) * (diff (id Z),x)) + (((id Z) . x) * (diff arctan ,x)) by A3, A5, A6, A7, FDIFF_1:29
.= ((arctan . x) * (((id Z) `| Z) . x)) + (((id Z) . x) * (diff arctan ,x)) by A5, A7, FDIFF_1:def 8
.= ((arctan . x) * 1) + (((id Z) . x) * (diff arctan ,x)) by A2, A4, A7, FDIFF_1:31
.= (arctan . x) + (x * (diff arctan ,x)) by A7, FUNCT_1:35
.= (arctan . x) + (x * (1 / (1 + (x ^2 )))) by A8, Th73
.= (arctan . x) + (x / (1 + (x ^2 ))) ;
hence (((id Z) (#) arctan ) `| Z) . x = (arctan . x) + (x / (1 + (x ^2 ))) ; :: thesis:

end;

hence ( (id Z) (#) arctan is_differentiable_on Z & ( for x being Real st x in Z holds
(((id Z) (#) arctan ) `| Z) . x = (arctan . x) + (x / (1 + (x ^2 ))) ) ) by A3, A5, A6, FDIFF_1:29; :: thesis: