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