theorem Th16: :: LEIBNIZ1:16

for n being Nat holds
( (Partial_Sums Leibniz_Series) . 1 = 2 / 3 & ( n is odd implies (Partial_Sums Leibniz_Series) . (n + 2) = ((Partial_Sums Leibniz_Series) . n) + (2 / (((4 * (n ^2)) + (16 * n)) + 15)) ) )