let r be Real; :: thesis: ( - 1 <= r & r <= 1 implies tan (arctan r) = r )
assume ( - 1 <= r & r <= 1 ) ; :: thesis: tan (arctan r) = r
then A1: r in [.(- 1),1.] by XXREAL_1:1;
then A2: r in dom (arctan | [.(- 1),1.]) by Th21, RELAT_1:91;
A3: arctan . r in [.(- (PI / 4)),(PI / 4).] by A1, Th47;
A4: [.(- (PI / 4)),(PI / 4).] c= ].(- (PI / 2)),(PI / 2).[ by Lm7, Lm8, XXREAL_2:def 12;
thus tan (arctan r) = tan . (arctan . r) by A3, A4, Th13
.= (tan | [.(- (PI / 4)),(PI / 4).]) . (arctan . r) by A1, Th47, FUNCT_1:72
.= (tan | [.(- (PI / 4)),(PI / 4).]) . ((arctan | [.(- 1),1.]) . r) by A1, FUNCT_1:72
.= ((tan | [.(- (PI / 4)),(PI / 4).]) * (arctan | [.(- 1),1.])) . r by A2, FUNCT_1:23
.= (id [.(- 1),1.]) . r by Th19, Th23, FUNCT_1:61
.= r by A1, FUNCT_1:35 ; :: thesis: verum