let Z be open Subset of REAL; :: thesis: ( arctan is_differentiable_on Z & ( for r being Real st r in Z holds
(arctan `| Z) . r = 1 / (1 + (r ^2)) ) )
A1: dom arctan = REAL by FUNCT_2:def 1;
A2: arctan is_differentiable_on Z by A1, FDIFF_1:28;
for r being Real st r in Z holds
(arctan `| Z) . r = 1 / (1 + (r ^2))

proof

let r be Real; :: thesis: ( r in Z implies (arctan `| Z) . r = 1 / (1 + (r ^2)) )
assume r in Z ; :: thesis: (arctan `| Z) . r = 1 / (1 + (r ^2))
hence (arctan `| Z) . r = diff (arctan,r) by A2, FDIFF_1:def 7
.= 1 / (1 + (r ^2)) by Th2 ;
:: thesis: verum

end;

hence ( arctan is_differentiable_on Z & ( for r being Real st r in Z holds
(arctan `| Z) . r = 1 / (1 + (r ^2)) ) ) by A1, FDIFF_1:28; :: thesis: verum