dom (sec | ].(PI / 2),PI.]) = (dom sec) /\ ].(PI / 2),PI.] by RELAT_1:61;
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 st th in ].(PI / 2),PI.] holds
(sec | ].(PI / 2),PI.]) . th = sec . th ) ) by FUNCT_1:47; :: thesis: verum