A1: [.(PI / 4),((3 / 4) * PI).] c= ].0,PI.[ by Lm9, Lm10, XXREAL_2:def 12;
rng (cot | [.(PI / 4),((3 / 4) * PI).]) c= rng (cot | ].0,PI.[)

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (cot | [.(PI / 4),((3 / 4) * PI).]) or y in rng (cot | ].0,PI.[) )
assume y in rng (cot | [.(PI / 4),((3 / 4) * PI).]) ; :: thesis: y in rng (cot | ].0,PI.[)
then y in cot .: [.(PI / 4),((3 / 4) * PI).] by RELAT_1:115;
then ex x being object st
( x in dom cot & x in [.(PI / 4),((3 / 4) * PI).] & y = cot . x ) by FUNCT_1:def 6;
then y in cot .: ].0,PI.[ by A1, FUNCT_1:def 6;
hence y in rng (cot | ].0,PI.[) by RELAT_1:115; :: thesis: verum

end;

hence [.(- 1),1.] c= dom arccot by Th22, FUNCT_1:33; :: thesis: verum