theorem :: SERIES_5:56

for s being Real_Sequence st ( for n being Nat st n >= 1 holds
( s . n = 1 + (1 / ((2 * n) + 1)) & s . 0 = 1 ) ) holds
for n being Nat st n >= 1 holds
(Partial_Product s) . n > (1 / 2) * (sqrt ((2 * n) + 3))