theorem :: BASEL_1:33

for n being Nat holds Basel-seq2 . n = (((PI ^2) / 6) * ((2 * n) / ((2 * n) + 1))) * (((2 * n) + 2) / ((2 * n) + 1))