dom (sec | [.0 ,(PI / 2).[) = (dom sec ) /\ [.0 ,(PI / 2).[ by RELAT_1:90;
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 number st th in [.0 ,(PI / 2).[ holds
(sec | [.0 ,(PI / 2).[) . th = sec . th ) ) by FUNCT_1:70; :: thesis: verum