let n be Nat; :: thesis: Basel-seq . n = 1 / (n ^2)
(rseq (0,1,1,0)) . n = 1 / n by Lm16;
hence Basel-seq . n = (1 / n) * (1 / n) by VALUED_1:5
.= (1 * 1) / (n * n) by XCMPLX_1:76
.= 1 / (n ^2) ;
:: thesis: verum