let n be Nat; :: thesis: Basel-seq1 . n = (((PI ^2) / 6) * ((2 * n) / ((2 * n) + 1))) * (((2 * n) - 1) / ((2 * n) + 1))
A1: (((PI ^2) / 6) (#) (rseq (2,0,2,1))) . n = ((PI ^2) / 6) * ((rseq (2,0,2,1)) . n) by VALUED_1:6;
( (rseq (2,0,2,1)) . n = ((2 * n) + 0) / ((2 * n) + 1) & (rseq (2,(- 1),2,1)) . n = ((2 * n) - 1) / ((2 * n) + 1) ) by Th5;
hence Basel-seq1 . n = (((PI ^2) / 6) * ((2 * n) / ((2 * n) + 1))) * (((2 * n) - 1) / ((2 * n) + 1)) by A1, VALUED_1:5; :: thesis: verum