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