let n be Nat; :: thesis: (Partial_Sums Basel-seq) . n >= 0
for n being Nat holds Basel-seq . n >= 0

proof

let n be Nat; :: thesis: Basel-seq . n >= 0
Basel-seq . n = 1 / (n ^2) by BASEL_1:31;
hence Basel-seq . n >= 0 ; :: thesis: verum

end;

hence (Partial_Sums Basel-seq) . n >= 0 by SERIES_3:34; :: thesis: verum