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