dom (sec | [.0,(PI / 2).[) = (dom sec) /\ [.0,(PI / 2).[ by RELAT_1:61;
then dom (sec | [.0,(PI / 2).[) = [.0,(PI / 2).[ by Th1, XBOOLE_1:28;
hence ( dom (sec | [.0,(PI / 2).[) = [.0,(PI / 2).[ & ( for th being Real st th in [.0,(PI / 2).[ holds
(sec | [.0,(PI / 2).[) . th = sec . th ) ) by FUNCT_1:47; :: thesis: verum