dom (sec | ].(PI / 2),PI .]) = (dom sec ) /\ ].(PI / 2),PI .] by RELAT_1:90;
then dom (sec | ].(PI / 2),PI .]) = ].(PI / 2),PI .] by Th2, XBOOLE_1:28;
hence ( dom (sec | ].(PI / 2),PI .]) = ].(PI / 2),PI .] & ( for th being real number st th in ].(PI / 2),PI .] holds
(sec | ].(PI / 2),PI .]) . th = sec . th ) ) by FUNCT_1:70; :: thesis: verum