let n be Nat; :: thesis: (Partial_Sums Basel-seq) . n < 5 / 3

per cases ( not n is trivial or n = 0 or n = 1 ) by NAT_2:28;

suppose not n is trivial ; :: thesis: (Partial_Sums Basel-seq) . n < 5 / 3

then Sum (Basel-seq,n) < 5 / 3 by Important;
hence (Partial_Sums Basel-seq) . n < 5 / 3 ; :: thesis: verum

end;

suppose n = 0 ; :: thesis: (Partial_Sums Basel-seq) . n < 5 / 3

then (Partial_Sums Basel-seq) . n = Basel-seq . 0 by SERIES_1:def 1
.= 1 / (0 ^2) by BASEL_1:31
.= 0 ;
hence (Partial_Sums Basel-seq) . n < 5 / 3 ; :: thesis: verum

end;

suppose F: n = 1 ; :: thesis: (Partial_Sums Basel-seq) . n < 5 / 3

(Partial_Sums Basel-seq) . (0 + 1) = ((Partial_Sums Basel-seq) . 0) + (Basel-seq . 1) by SERIES_1:def 1
.= (Basel-seq . 0) + (Basel-seq . 1) by SERIES_1:def 1
.= (1 / (0 ^2)) + (Basel-seq . 1) by BASEL_1:31
.= 0 + (Basel-seq . 1)
.= 0 + (1 / (1 ^2)) by BASEL_1:31
.= 1 ;
hence (Partial_Sums Basel-seq) . n < 5 / 3 by F; :: thesis: verum

end;

end;