let Z be open Subset of REAL; :: thesis: ( Z c= ].(- 1),1.[ implies ( (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))) ) ) )
assume A1: Z c= ].(- 1),1.[ ; :: thesis: ( (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))) ) )
A2: Z c= dom (id Z) by FUNCT_1:17;
].(- 1),1.[ c= [.(- 1),1.] by XXREAL_1:25;
then ].(- 1),1.[ c= dom arctan by Th23;
then Z c= dom arctan by A1;
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:18;
then A5: id Z is_differentiable_on Z by A2, FDIFF_1:23;
A6: arctan is_differentiable_on Z by A1, Th81;
for x being Real st x in Z holds
(((id Z) (#) arctan) `| Z) . x = (arctan . x) + (x / (1 + (x ^2)))

proof

let x be Real; :: thesis: ( x in Z implies (((id Z) (#) arctan) `| Z) . x = (arctan . x) + (x / (1 + (x ^2))) )
assume A7: x in Z ; :: thesis: (((id Z) (#) arctan) `| Z) . x = (arctan . x) + (x / (1 + (x ^2)))
then A8: - 1 < x by A1, XXREAL_1:4;
A9: x < 1 by A1, A7, 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:21
.= ((arctan . x) * (((id Z) `| Z) . x)) + (((id Z) . x) * (diff (arctan,x))) by A5, A7, FDIFF_1:def 7
.= ((arctan . x) * 1) + (((id Z) . x) * (diff (arctan,x))) by A2, A4, A7, FDIFF_1:23
.= (arctan . x) + (x * (diff (arctan,x))) by A7, FUNCT_1:18
.= (arctan . x) + (x * (1 / (1 + (x ^2)))) by A8, A9, Th75
.= (arctan . x) + (x / (1 + (x ^2))) ;
hence (((id Z) (#) arctan) `| Z) . x = (arctan . x) + (x / (1 + (x ^2))) ; :: thesis: verum

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:21; :: thesis: verum