[.(- (PI / 4)),(PI / 4).] c= ].(- (PI / 2)),(PI / 2).[ by Lm7, Lm8, XXREAL_2:def 12;
then (tan | ].(- (PI / 2)),(PI / 2).[) | [.(- (PI / 4)),(PI / 4).] = tan | [.(- (PI / 4)),(PI / 4).] by RELAT_1:74;
hence tan | [.(- (PI / 4)),(PI / 4).] is one-to-one ; :: thesis: verum