theorem :: SERIES_4:20

for n being Nat
for s being Real_Sequence st ( for n being Nat holds s . n = 1 / ((2 -Root (n + 1)) + (2 -Root n)) ) holds
(Partial_Sums s) . n = 2 -Root (n + 1)