dom (cosec | ].0 ,(PI / 2).]) = ].0 ,(PI / 2).] by Th4, RELAT_1:91;
hence rng arccosec2 = ].0 ,(PI / 2).] by FUNCT_1:55; :: thesis: verum