let n be Nat; Basel-seq2 . n = (((PI ^2) / 6) * ((2 * n) / ((2 * n) + 1))) * (((2 * n) + 2) / ((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,2,2,1)) . n = ((2 * n) + 2) / ((2 * n) + 1) )
by Th5;
hence
Basel-seq2 . n = (((PI ^2) / 6) * ((2 * n) / ((2 * n) + 1))) * (((2 * n) + 2) / ((2 * n) + 1))
by A1, VALUED_1:5; verum