set g = arctan ;
set f = tan | ].(- (PI / 2)),(PI / 2).[;
A1: dom ((tan | ].(- (PI / 2)),(PI / 2).[) " ) = rng (tan | ].(- (PI / 2)),(PI / 2).[) by FUNCT_1:55
.= tan .: ].(- (PI / 2)),(PI / 2).[ by RELAT_1:148 ;
dom (tan | ].(- (PI / 2)),(PI / 2).[) = (dom tan ) /\ ].(- (PI / 2)),(PI / 2).[ by RELAT_1:90;
then A2: ].(- (PI / 2)),(PI / 2).[ c= dom (tan | ].(- (PI / 2)),(PI / 2).[) by Th1, XBOOLE_1:19;
A3: tan | ].(- (PI / 2)),(PI / 2).[ is_differentiable_on ].(- (PI / 2)),(PI / 2).[ by Lm1, FDIFF_2:16;

A4: now

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

end;

(tan | ].(- (PI / 2)),(PI / 2).[) | ].(- (PI / 2)),(PI / 2).[ = tan | ].(- (PI / 2)),(PI / 2).[ by RELAT_1:101;
hence arctan is_differentiable_on tan .: ].(- (PI / 2)),(PI / 2).[ by A1, A3, A2, A4, FDIFF_2:48; :: thesis: verum