[.(- (PI / 4)),(PI / 4).] c= ].(- (PI / 2)),(PI / 2).[ by Lm7, Lm8, XXREAL_2:def 12;
hence dom (tan | [.(- (PI / 4)),(PI / 4).]) = [.(- (PI / 4)),(PI / 4).] by Th1, RELAT_1:62, XBOOLE_1:1; :: thesis: verum