let r be Real; :: thesis: diff (arctan,r) = 1 / (1 + (r ^2))
set g = arctan ;
set f = tan | ].(- (PI / 2)),(PI / 2).[;
set x = arctan . r;
A1: ((sin . (arctan . r)) ^2) + ((cos . (arctan . r)) ^2) = 1 by SIN_COS:28;
A2: tan | ].(- (PI / 2)),(PI / 2).[ is_differentiable_on ].(- (PI / 2)),(PI / 2).[ by Lm1, FDIFF_2:16;

A3: now :: thesis: for x0 being Real st x0 in ].(- (PI / 2)),(PI / 2).[ holds
0 < diff ((tan | ].(- (PI / 2)),(PI / 2).[),x0)

A4: for x0 being Real st x0 in ].(- (PI / 2)),(PI / 2).[ holds
1 / ((cos . x0) ^2) > 0

proof

let x0 be Real; :: thesis: ( x0 in ].(- (PI / 2)),(PI / 2).[ implies 1 / ((cos . x0) ^2) > 0 )
assume x0 in ].(- (PI / 2)),(PI / 2).[ ; :: thesis: 1 / ((cos . x0) ^2) > 0
then 0 < cos . x0 by COMPTRIG:11;
hence 1 / ((cos . x0) ^2) > 0 ; :: thesis: verum

end;

let x0 be Real; :: thesis: ( x0 in ].(- (PI / 2)),(PI / 2).[ implies 0 < diff ((tan | ].(- (PI / 2)),(PI / 2).[),x0) )
assume A5: x0 in ].(- (PI / 2)),(PI / 2).[ ; :: thesis: 0 < diff ((tan | ].(- (PI / 2)),(PI / 2).[),x0)
diff ((tan | ].(- (PI / 2)),(PI / 2).[),x0) = ((tan | ].(- (PI / 2)),(PI / 2).[) `| ].(- (PI / 2)),(PI / 2).[) . x0 by A2, A5, FDIFF_1:def 7
.= (tan `| ].(- (PI / 2)),(PI / 2).[) . x0 by Lm1, FDIFF_2:16
.= diff (tan,x0) by A5, Lm1, FDIFF_1:def 7
.= 1 / ((cos . x0) ^2) by A5, Lm2 ;
hence 0 < diff ((tan | ].(- (PI / 2)),(PI / 2).[),x0) by A5, A4; :: thesis: verum

end;

A6: ( rng arctan = dom (tan | ].(- (PI / 2)),(PI / 2).[) & dom arctan = rng (tan | ].(- (PI / 2)),(PI / 2).[) ) by FUNCT_1:33;
set x = arctan . r;
A7: ( dom arctan = REAL & r in REAL ) by FUNCT_2:def 1, XREAL_0:def 1;
then A8: arctan . r in dom (tan | ].(- (PI / 2)),(PI / 2).[) by A6, FUNCT_1:def 3;
then A9: arctan . r in ].(- (PI / 2)),(PI / 2).[ by RELAT_1:57;
A10: cos (arctan . r) <> 0 by A8, RELAT_1:57, COMPTRIG:11;
A11: r = (tan | ].(- (PI / 2)),(PI / 2).[) . (arctan . r) by A7, A6, FUNCT_1:32
.= tan . (arctan . r) by A8, FUNCT_1:47
.= tan (arctan . r) by A10, SIN_COS9:15
.= (sin (arctan . r)) / (cos (arctan . r)) by SIN_COS4:def 1 ;
dom (tan | ].(- (PI / 2)),(PI / 2).[) = (dom tan) /\ ].(- (PI / 2)),(PI / 2).[ by RELAT_1:61;
then A12: ].(- (PI / 2)),(PI / 2).[ c= dom (tan | ].(- (PI / 2)),(PI / 2).[) by SIN_COS9:1, XBOOLE_1:19;
A13: (tan | ].(- (PI / 2)),(PI / 2).[) | ].(- (PI / 2)),(PI / 2).[ = tan | ].(- (PI / 2)),(PI / 2).[ ;
r * (cos (arctan . r)) = sin (arctan . r) by A10, A11, XCMPLX_1:87;
then A14: 1 = ((cos (arctan . r)) ^2) * ((r ^2) + 1) by A1;
tan | ].(- (PI / 2)),(PI / 2).[ is_differentiable_on ].(- (PI / 2)),(PI / 2).[ by Lm1, FDIFF_2:16;
then diff ((tan | ].(- (PI / 2)),(PI / 2).[),(arctan . r)) = ((tan | ].(- (PI / 2)),(PI / 2).[) `| ].(- (PI / 2)),(PI / 2).[) . (arctan . r) by A9, FDIFF_1:def 7
.= (tan `| ].(- (PI / 2)),(PI / 2).[) . (arctan . r) by Lm1, FDIFF_2:16
.= diff (tan,(arctan . r)) by A9, Lm1, FDIFF_1:def 7
.= 1 / ((cos (arctan . r)) ^2) by A8, RELAT_1:57, Lm2 ;
then diff (arctan,r) = 1 / (1 / ((cos (arctan . r)) ^2)) by A2, A3, A13, A12, A7, FDIFF_2:48
.= 1 / ((r ^2) + 1) by A14, XCMPLX_1:73 ;
hence diff (arctan,r) = 1 / (1 + (r ^2)) ; :: thesis: verum