for m being Nat holds
( len (x_r-seq m) = m & ( for k being Nat st 1 <= k & k <= m holds
(x_r-seq m) . k = (k * PI) / ((2 * m) + 1) ) )