let r be Real; :: thesis: ( - 1 <= r & r <= 1 implies diff arctan ,r = 1 / (1 + (r ^2 )) )
set f = tan | ].(- (PI / 2)),(PI / 2).[;
set g = arctan ;
set x = arctan . r;
set X = tan .: ].(- (PI / 2)),(PI / 2).[;
assume A1: ( - 1 <= r & r <= 1 ) ; :: thesis: diff arctan ,r = 1 / (1 + (r ^2 ))
then A2: r in [.(- 1),1.] by XXREAL_1:1;
then A3: arctan . r in [.(- (PI / 4)),(PI / 4).] by Th47;
A4: [.(- (PI / 4)),(PI / 4).] c= ].(- (PI / 2)),(PI / 2).[ by Lm7, Lm8, XXREAL_2:def 12;
A5: tan | ].(- (PI / 2)),(PI / 2).[ is_differentiable_on ].(- (PI / 2)),(PI / 2).[ by Lm1, FDIFF_2:16;
A6: diff (tan | ].(- (PI / 2)),(PI / 2).[),(arctan . r) = ((tan | ].(- (PI / 2)),(PI / 2).[) `| ].(- (PI / 2)),(PI / 2).[) . (arctan . r) by A3, A4, A5, FDIFF_1:def 8
.= (tan `| ].(- (PI / 2)),(PI / 2).[) . (arctan . r) by Lm1, FDIFF_2:16
.= diff tan ,(arctan . r) by A3, A4, Lm1, FDIFF_1:def 8
.= 1 / ((cos (arctan . r)) ^2 ) by A3, A4, Lm3 ;
A7: cos (arctan . r) <> 0 by A3, A4, COMPTRIG:27;
B8: ((sin . (arctan . r)) ^2 ) + ((cos . (arctan . r)) ^2 ) = 1 by SIN_COS:31;
arctan . r = arctan r ;
then r = tan (arctan . r) by A1, Th49
.= (sin (arctan . r)) / (cos (arctan . r)) by SIN_COS4:def 1 ;
then r * (cos (arctan . r)) = sin (arctan . r) by A7, XCMPLX_1:88;
then A9: 1 = ((cos (arctan . r)) ^2 ) * ((r ^2 ) + 1) by B8;
A13: tan | ].(- (PI / 2)),(PI / 2).[ is_differentiable_on ].(- (PI / 2)),(PI / 2).[ by Lm1, FDIFF_2:16;

A14: now

let x0 be Real; :: thesis: ( x0 in ].(- (PI / 2)),(PI / 2).[ implies 0 < diff (tan | ].(- (PI / 2)),(PI / 2).[),x0 )
assume A15: x0 in ].(- (PI / 2)),(PI / 2).[ ; :: thesis: 0 < diff (tan | ].(- (PI / 2)),(PI / 2).[),x0
A16: diff (tan | ].(- (PI / 2)),(PI / 2).[),x0 = ((tan | ].(- (PI / 2)),(PI / 2).[) `| ].(- (PI / 2)),(PI / 2).[) . x0 by A13, A15, FDIFF_1:def 8
.= (tan `| ].(- (PI / 2)),(PI / 2).[) . x0 by Lm1, FDIFF_2:16
.= diff tan ,x0 by A15, Lm1, FDIFF_1:def 8
.= 1 / ((cos . x0) ^2 ) by A15, Lm3 ;
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 A17: (cos . x0) ^2 > 0 by SQUARE_1:74;
1 / ((cos . x0) ^2 ) > 0 / ((cos . x0) ^2 ) by A17, XREAL_1:76;
hence 1 / ((cos . x0) ^2 ) > 0 ; :: thesis: verum

end;

hence 0 < diff (tan | ].(- (PI / 2)),(PI / 2).[),x0 by A15, A16; :: thesis: verum

end;

A18: (tan | ].(- (PI / 2)),(PI / 2).[) | ].(- (PI / 2)),(PI / 2).[ = tan | ].(- (PI / 2)),(PI / 2).[ by RELAT_1:101;
dom (tan | ].(- (PI / 2)),(PI / 2).[) = (dom tan ) /\ ].(- (PI / 2)),(PI / 2).[ by RELAT_1:90;
then ].(- (PI / 2)),(PI / 2).[ c= dom (tan | ].(- (PI / 2)),(PI / 2).[) by Th1, XBOOLE_1:19;
then diff arctan ,r = 1 / (1 / ((cos (arctan . r)) ^2 )) by A2, A6, A13, A14, A18, Th21, FDIFF_2:48
.= 1 / ((r ^2 ) + 1) by A9, XCMPLX_1:74 ;
hence diff arctan ,r = 1 / (1 + (r ^2 )) ; :: thesis: verum