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