for m being Nat holds Sum ((sqr (x_r-seq m)) ") = ((((2 * m) + 1) ^2) / (PI ^2)) * (Sum (Basel-seq,m))