let r be Real; ( - (PI / 2) < r & r < PI / 2 implies ( arctan (tan . r) = r & arctan (tan r) = r ) )
assume that
A1:
- (PI / 2) < r
and
A2:
r < PI / 2
; ( arctan (tan . r) = r & arctan (tan r) = r )
A3:
dom (tan | ].(- (PI / 2)),(PI / 2).[) = ].(- (PI / 2)),(PI / 2).[
by Th1, RELAT_1:62;
A4:
r in ].(- (PI / 2)),(PI / 2).[
by A1, A2, XXREAL_1:4;
then arctan (tan . r) =
arctan . ((tan | ].(- (PI / 2)),(PI / 2).[) . r)
by FUNCT_1:49
.=
(id ].(- (PI / 2)),(PI / 2).[) . r
by A4, A3, Th31, FUNCT_1:13
.=
r
by A4, FUNCT_1:18
;
hence
( arctan (tan . r) = r & arctan (tan r) = r )
by A4, Th13; verum