let r be Real; :: thesis: ( - (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 ; :: thesis: ( 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; :: thesis: verum