dom (cosec | [.(- (PI / 2)),0 .[) = [.(- (PI / 2)),0 .[ by Th3, RELAT_1:91;
hence rng arccosec1 = [.(- (PI / 2)),0 .[ by FUNCT_1:55; :: thesis: verum