set h = tan | ].(- (PI / 2)),(PI / 2).[;
A1:
[.(- (PI / 4)),(PI / 4).] c= ].(- (PI / 2)),(PI / 2).[
by Lm7, Lm8, XXREAL_2:def 12;
then (tan | [.(- (PI / 4)),(PI / 4).]) " =
((tan | ].(- (PI / 2)),(PI / 2).[) | [.(- (PI / 4)),(PI / 4).]) "
by RELAT_1:74
.=
((tan | ].(- (PI / 2)),(PI / 2).[) ") | ((tan | ].(- (PI / 2)),(PI / 2).[) .: [.(- (PI / 4)),(PI / 4).])
by RFUNCT_2:17
.=
((tan | ].(- (PI / 2)),(PI / 2).[) ") | (rng ((tan | ].(- (PI / 2)),(PI / 2).[) | [.(- (PI / 4)),(PI / 4).]))
by RELAT_1:115
.=
((tan | ].(- (PI / 2)),(PI / 2).[) ") | [.(- 1),1.]
by A1, Th21, RELAT_1:74
;
hence
arctan | [.(- 1),1.] = (tan | [.(- (PI / 4)),(PI / 4).]) "
; verum