let n be Nat; :: thesis: for s being Real_Sequence st ( for n being Nat holds s . n = 1 / ((n + 1) ^2) ) holds
(Partial_Sums s) . n < 2
let s be Real_Sequence; :: thesis: ( ( for n being Nat holds s . n = 1 / ((n + 1) ^2) ) implies (Partial_Sums s) . n < 2 )
assume for n being Nat holds s . n = 1 / ((n + 1) ^2) ; :: thesis: (Partial_Sums s) . n < 2
then A1: (Partial_Sums s) . n <= 2 - (1 / (n + 1)) by Th48;
(- (1 / (n + 1))) + 2 < 0 + 2 by XREAL_1:8;
hence (Partial_Sums s) . n < 2 by A1, XXREAL_0:2; :: thesis: verum