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