theorem Th29: :: BASEL_1:31

for n being Nat holds Basel-seq . n = 1 / (n ^2)