theorem :: SERIES_2:32

for s being Real_Sequence st ( for n being Nat holds s . n = ((n + 1) * (2 |^ n)) / ((n + 2) * (n + 3)) ) holds
for n being Nat holds (Partial_Sums s) . n = ((2 |^ (n + 1)) / (n + 3)) - (1 / 2)