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 set ; :: 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:148;
then consider x being set such that
A3: x in dom cot and
A4: x in [.(PI / 4),((3 / 4) * PI ).] and
A5: y = cot . x by FUNCT_1:def 12;
y in cot .: ].0 ,PI .[ by A1, A3, A4, A5, FUNCT_1:def 12;
hence y in rng (cot | ].0 ,PI .[) by RELAT_1:148; :: thesis: verum

end;

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