let r be Real; :: thesis: ( - 1 <= r & r <= 1 implies tan (arctan r) = r )
A1: [.(- (PI / 4)),(PI / 4).] c= ].(- (PI / 2)),(PI / 2).[ by Lm7, Lm8, XXREAL_2:def 12;
assume that
A2: - 1 <= r and
A3: r <= 1 ; :: thesis: tan (arctan r) = r
A4: r in [.(- 1),1.] by A2, A3, XXREAL_1:1;
then A5: r in dom (arctan | [.(- 1),1.]) by Th23, RELAT_1:62;
arctan . r in [.(- (PI / 4)),(PI / 4).] by A4, Th49;
hence tan (arctan r) = tan . (arctan . r) by A1, Th13
.= (tan | [.(- (PI / 4)),(PI / 4).]) . (arctan . r) by A4, Th49, FUNCT_1:49
.= (tan | [.(- (PI / 4)),(PI / 4).]) . ((arctan | [.(- 1),1.]) . r) by A4, FUNCT_1:49
.= ((tan | [.(- (PI / 4)),(PI / 4).]) * (arctan | [.(- 1),1.])) . r by A5, FUNCT_1:13
.= (id [.(- 1),1.]) . r by Th21, Th25, FUNCT_1:39
.= r by A4, FUNCT_1:18 ;
:: thesis: verum