theorem :: SERIES_5:49

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