let r be Real; :: thesis: ( - (PI / 2) < r & r < PI / 2 implies ( arctan (tan . r) = r & arctan (tan r) = r ) )
assume ( - (PI / 2) < r & r < PI / 2 ) ; :: thesis: ( arctan (tan . r) = r & arctan (tan r) = r )
then A1: r in ].(- (PI / 2)),(PI / 2).[ by XXREAL_1:4;
A2: dom (tan | ].(- (PI / 2)),(PI / 2).[) = ].(- (PI / 2)),(PI / 2).[ by Th1, RELAT_1:91;
arctan (tan . r) = arctan . ((tan | ].(- (PI / 2)),(PI / 2).[) . r) by A1, FUNCT_1:72
.= (id ].(- (PI / 2)),(PI / 2).[) . r by A1, A2, Th29, FUNCT_1:23
.= r by A1, FUNCT_1:35 ;
hence ( arctan (tan . r) = r & arctan (tan r) = r ) by A1, Th13; :: thesis: verum