theorem :: SERIES_5:54

for s being Real_Sequence st ( for n being Nat st n >= 1 holds
( s . n = sqrt n & s . 0 = 0 ) ) holds
for n being Nat st n >= 1 holds
(Partial_Sums s) . n < ((1 / 6) * ((4 * n) + 3)) * (sqrt n)