:: deftheorem defines Basel-seq1 BASEL_1:def 7 :
Basel-seq1 = (((PI ^2) / 6) (#) (rseq (2,0,2,1))) (#) (rseq (2,(- 1),2,1));