lim (((PI ^2) / 6) (#) (rseq (2,0,2,1))) = ((PI ^2) / 6) * (lim (rseq (2,0,2,1))) by SEQ_2:8;
hence lim Basel-seq1 = (PI ^2) / 6 by Lm17, Lm18, SEQ_2:15; :: thesis: (PI ^2) / 6 = lim Basel-seq2
lim (((PI ^2) / 6) (#) (rseq (2,0,2,1))) = ((PI ^2) / 6) * (lim (rseq (2,0,2,1))) by SEQ_2:8;
hence (PI ^2) / 6 = lim Basel-seq2 by Lm17, Lm19, SEQ_2:15; :: thesis: verum