theorem :: BASEL_1:26
for m being Nat holds sqr (cosec (x_r-seq m)) = 1 + (sqr (cot (x_r-seq m)))