dom (sec | ].(PI / 2),PI .]) = ].(PI / 2),PI .] by Th2, RELAT_1:91;
hence rng arcsec2 = ].(PI / 2),PI .] by FUNCT_1:55; :: thesis: verum