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