let s be Real_Sequence; :: thesis: ( ( for n being Element of NAT holds s . n = 1 / (sqrt (n + 1)) ) implies for n being Element of NAT holds (Partial_Sums s) . n < 2 * (sqrt (n + 1)) )
assume A1: for n being Element of NAT holds s . n = 1 / (sqrt (n + 1)) ; :: thesis: for n being Element of NAT holds (Partial_Sums s) . n < 2 * (sqrt (n + 1))
defpred S₁[ Element of NAT ] means (Partial_Sums s) . $1 < 2 * (sqrt ($1 + 1));
(Partial_Sums s) . 0 = s . 0 by SERIES_1:def 1
.= 1 / (sqrt (0 + 1)) by A1
.= 1 by SQUARE_1:83 ;
then A2: S₁[ 0 ] by SQUARE_1:83;
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 * (sqrt (n + 1)) ; :: thesis: S₁[n + 1]
then A4: ((Partial_Sums s) . n) + (1 / (sqrt (n + 2))) < (2 * (sqrt (n + 1))) + (1 / (sqrt (n + 2))) by XREAL_1:10;
A5: sqrt (n + 2) > 0 by SQUARE_1:93;
((4 * (n ^2 )) + (12 * n)) + 8 < ((4 * (n ^2 )) + (12 * n)) + 9 by XREAL_1:10;
then sqrt (4 * ((n + 2) * (n + 1))) < sqrt (((2 * n) + 3) ^2 ) by SQUARE_1:95;
then 2 * (sqrt ((n + 2) * (n + 1))) < sqrt (((2 * n) + 3) ^2 ) by SQUARE_1:85, SQUARE_1:97;
then 2 * (sqrt ((n + 2) * (n + 1))) < (2 * n) + 3 by SQUARE_1:89;
then (2 * (sqrt ((n + 2) * (n + 1)))) + 1 < ((2 * n) + 3) + 1 by XREAL_1:10;
then (2 * ((sqrt (n + 2)) * (sqrt (n + 1)))) + 1 < 2 * (n + 2) by SQUARE_1:97;
then (2 * ((sqrt (n + 2)) * (sqrt (n + 1)))) + 1 < 2 * (sqrt ((n + 2) ^2 )) by SQUARE_1:89;
then ((2 * ((sqrt (n + 2)) * (sqrt (n + 1)))) + 1) / (sqrt (n + 2)) < (2 * (sqrt ((n + 2) * (n + 2)))) / (sqrt (n + 2)) by A5, XREAL_1:76;
then ((2 * ((sqrt (n + 2)) * (sqrt (n + 1)))) + 1) / (sqrt (n + 2)) < (2 * ((sqrt (n + 2)) * (sqrt (n + 2)))) / (sqrt (n + 2)) by SQUARE_1:97;
then ((2 * ((sqrt (n + 2)) * (sqrt (n + 1)))) + 1) / (sqrt (n + 2)) < ((2 * (sqrt (n + 2))) * (sqrt (n + 2))) / (sqrt (n + 2)) ;
then ((2 * ((sqrt (n + 2)) * (sqrt (n + 1)))) + 1) / (sqrt (n + 2)) < 2 * (sqrt (n + 2)) by A5, XCMPLX_1:90;
then (((2 * (sqrt (n + 1))) * (sqrt (n + 2))) / (sqrt (n + 2))) + (1 / (sqrt (n + 2))) < 2 * (sqrt (n + 2)) by XCMPLX_1:63;
then (2 * (sqrt (n + 1))) + (1 / (sqrt (n + 2))) < 2 * (sqrt (n + 2)) by A5, XCMPLX_1:90;
then ((Partial_Sums s) . n) + (1 / (sqrt ((n + 1) + 1))) < 2 * (sqrt (n + 2)) by A4, XXREAL_0:2;
then ((Partial_Sums s) . n) + (s . (n + 1)) < 2 * (sqrt (n + 2)) by A1;
hence S₁[n + 1] by SERIES_1:def 1; :: 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 * (sqrt (n + 1)) ; :: thesis: verum