let r be Real; :: thesis: ( - 1 <= r & r <= 1 implies diff arctan ,r = 1 / (1 + (r ^2 )) )
set X = tan .: ].(- (PI / 2)),(PI / 2).[;
set g = arctan ;
set f = tan | ].(- (PI / 2)),(PI / 2).[;
set x = arctan . r;
assume that
A1: - 1 <= r and
A2: r <= 1 ; :: thesis: diff arctan ,r = 1 / (1 + (r ^2 ))
A3: ((sin . (arctan . r)) ^2 ) + ((cos . (arctan . r)) ^2 ) = 1 by SIN_COS:31;
A4: tan | ].(- (PI / 2)),(PI / 2).[ is_differentiable_on ].(- (PI / 2)),(PI / 2).[ by Lm1, FDIFF_2:16;

A5: now

A6: 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:27;
then (cos . x0) ^2 > 0 by SQUARE_1:74;
then 1 / ((cos . x0) ^2 ) > 0 / ((cos . x0) ^2 ) by XREAL_1:76;
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 A7: 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 A4, A7, FDIFF_1:def 8
.= (tan `| ].(- (PI / 2)),(PI / 2).[) . x0 by Lm1, FDIFF_2:16
.= diff tan ,x0 by A7, Lm1, FDIFF_1:def 8
.= 1 / ((cos . x0) ^2 ) by A7, Lm3 ;
hence 0 < diff (tan | ].(- (PI / 2)),(PI / 2).[),x0 by A7, A6; :: thesis: verum

end;

A8: r in [.(- 1),1.] by A1, A2, XXREAL_1:1;
then A9: arctan . r in [.(- (PI / 4)),(PI / 4).] by Th49;
arctan . r = arctan r ;
then A10: r = tan (arctan . r) by A1, A2, Th51
.= (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:90;
then A11: ].(- (PI / 2)),(PI / 2).[ c= dom (tan | ].(- (PI / 2)),(PI / 2).[) by Th1, XBOOLE_1:19;
A12: (tan | ].(- (PI / 2)),(PI / 2).[) | ].(- (PI / 2)),(PI / 2).[ = tan | ].(- (PI / 2)),(PI / 2).[ by RELAT_1:101;
A13: [.(- (PI / 4)),(PI / 4).] c= ].(- (PI / 2)),(PI / 2).[ by Lm7, Lm8, XXREAL_2:def 12;
then cos (arctan . r) <> 0 by A9, COMPTRIG:27;
then r * (cos (arctan . r)) = sin (arctan . r) by A10, XCMPLX_1:88;
then A14: 1 = ((cos (arctan . r)) ^2 ) * ((r ^2 ) + 1) by A3;
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, A13, FDIFF_1:def 8
.= (tan `| ].(- (PI / 2)),(PI / 2).[) . (arctan . r) by Lm1, FDIFF_2:16
.= diff tan ,(arctan . r) by A9, A13, Lm1, FDIFF_1:def 8
.= 1 / ((cos (arctan . r)) ^2 ) by A9, A13, Lm3 ;
then diff arctan ,r = 1 / (1 / ((cos (arctan . r)) ^2 )) by A8, A4, A5, A12, A11, Th23, FDIFF_2:48
.= 1 / ((r ^2 ) + 1) by A14, XCMPLX_1:74 ;
hence diff arctan ,r = 1 / (1 + (r ^2 )) ; :: thesis: verum