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