theorem :: SERIES_5:47

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