theorem :: BASEL_1:28

for n being Nat holds sqr (cot (x_r-seq n)) is one-to-one