theorem :: BASEL_1:32

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