dom (tan | ].(- (PI / 2)),(PI / 2).[) = ].(- (PI / 2)),(PI / 2).[ by Th1, RELAT_1:62;
hence rng arctan = ].(- (PI / 2)),(PI / 2).[ by FUNCT_1:33; :: thesis: verum