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

(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