dom arctan = REAL by Th1, FUNCT_1:33;
hence arctan is total by PARTFUN1:def 2; :: thesis: verum