set f = tan | ].(- (PI / 2)),(PI / 2).[;
A1: (tan | ].(- (PI / 2)),(PI / 2).[) .: ].(- (PI / 2)),(PI / 2).[ =
rng ((tan | ].(- (PI / 2)),(PI / 2).[) | ].(- (PI / 2)),(PI / 2).[)
by RELAT_1:115
.=
rng (tan | ].(- (PI / 2)),(PI / 2).[)
by RELAT_1:73
.=
tan .: ].(- (PI / 2)),(PI / 2).[
by RELAT_1:115
;
(tan | ].(- (PI / 2)),(PI / 2).[) | ].(- (PI / 2)),(PI / 2).[ = tan | ].(- (PI / 2)),(PI / 2).[
by RELAT_1:73;
hence
arctan | (tan .: ].(- (PI / 2)),(PI / 2).[) is increasing
by A1, Th7, FCONT_3:9; verum