let s be Real_Sequence; :: thesis: ( ( for n being Element of NAT holds s . n = 1 / ((n + 1) ^2 ) ) implies for n being Element of NAT holds (Partial_Sums s) . n <= 2 - (1 / (n + 1)) )
assume A1: for n being Element of NAT holds s . n = 1 / ((n + 1) ^2 ) ; :: thesis: for n being Element of NAT holds (Partial_Sums s) . n <= 2 - (1 / (n + 1))
defpred S₁[ Element of NAT ] means (Partial_Sums s) . $1 <= 2 - (1 / ($1 + 1));
(Partial_Sums s) . 0 = s . 0 by SERIES_1:def 1
.= 1 / ((0 + 1) ^2 ) by A1
.= 1 ;
then A2: S₁[ 0 ] ;
A3: for n being Element of NAT st S₁[n] holds
S₁[n + 1]

proof

let n be Element of NAT ; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume (Partial_Sums s) . n <= 2 - (1 / (n + 1)) ; :: thesis: S₁[n + 1]
then A4: ((Partial_Sums s) . n) + (1 / ((n + 2) ^2 )) <= (2 - (1 / (n + 1))) + (1 / ((n + 2) ^2 )) by XREAL_1:9;
((n ^2 ) + (3 * n)) + 3 > ((n ^2 ) + (3 * n)) + 2 by XREAL_1:10;
then (((n ^2 ) + (3 * n)) + 3) / ((n + 1) * ((n + 2) ^2 )) > ((n + 2) * (n + 1)) / (((n + 2) ^2 ) * (n + 1)) by XREAL_1:76;
then (((n ^2 ) + (3 * n)) + 3) / ((n + 1) * ((n + 2) ^2 )) > (n + 2) / ((n + 2) * (n + 2)) by XCMPLX_1:92;
then (((n ^2 ) + (3 * n)) + 3) / ((n + 1) * ((n + 2) ^2 )) > ((n + 2) / (n + 2)) / (n + 2) by XCMPLX_1:79;
then (((n ^2 ) + (3 * n)) + 3) / ((n + 1) * ((n + 2) ^2 )) > 1 / (n + 2) by XCMPLX_1:60;
then (- 1) * ((((n ^2 ) + (3 * n)) + 3) / ((n + 1) * ((n + 2) ^2 ))) < (- 1) * (1 / (n + 2)) by XREAL_1:71;
then A6: (- ((((n ^2 ) + (3 * n)) + 3) / ((n + 1) * ((n + 2) ^2 )))) + 2 < (- (1 / (n + 2))) + 2 by XREAL_1:10;
(Partial_Sums s) . (n + 1) = ((Partial_Sums s) . n) + (s . (n + 1)) by SERIES_1:def 1
.= ((Partial_Sums s) . n) + (1 / (((n + 1) + 1) ^2 )) by A1 ;
then (Partial_Sums s) . (n + 1) <= 2 - ((1 / (n + 1)) - (1 / ((n + 2) ^2 ))) by A4;
then (Partial_Sums s) . (n + 1) <= 2 - (((1 * ((n + 2) ^2 )) - (1 * (n + 1))) / ((n + 1) * ((n + 2) ^2 ))) by XCMPLX_1:131;
hence S₁[n + 1] by A6, XXREAL_0:2; :: thesis: verum

end;

for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A2, A3);
hence for n being Element of NAT holds (Partial_Sums s) . n <= 2 - (1 / (n + 1)) ; :: thesis: verum