theorem Telescoping: :: MOEBIUS3:24

for a, b, s being Real_Sequence st ( for n being Nat holds s . n = (a . n) + (b . n) ) & ( for k being Nat holds b . k = - (a . (k + 1)) ) holds
for n being Nat holds (Partial_Sums s) . n = (a . 0) + (b . n)