theorem :: BASEL_1:24

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