theorem :: MOEBIUS3:30

for n being Nat holds (Partial_Sums Reci-seq1) . n = (- 2) + (- (1 / (n + (1 / 2))))