let s be Real_Sequence; :: thesis: ( ( for n being Nat holds s . n = 1 / (sqrt (n + 1)) ) implies for n being Nat holds (Partial_Sums s) . n < 2 * (sqrt (n + 1)) )
defpred S₁[ Nat] means (Partial_Sums s) . $1 < 2 * (sqrt ($1 + 1));
assume A1: for n being Nat holds s . n = 1 / (sqrt (n + 1)) ; :: thesis: for n being Nat holds (Partial_Sums s) . n < 2 * (sqrt (n + 1))
A2: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
A3: sqrt (n + 2) > 0 by SQUARE_1:25;
((4 * (n ^2)) + (12 * n)) + 8 < ((4 * (n ^2)) + (12 * n)) + 9 by XREAL_1:8;
then sqrt (4 * ((n + 2) * (n + 1))) < sqrt (((2 * n) + 3) ^2) by SQUARE_1:27;
then 2 * (sqrt ((n + 2) * (n + 1))) < sqrt (((2 * n) + 3) ^2) by SQUARE_1:20, SQUARE_1:29;
then 2 * (sqrt ((n + 2) * (n + 1))) < (2 * n) + 3 by SQUARE_1:22;
then (2 * (sqrt ((n + 2) * (n + 1)))) + 1 < ((2 * n) + 3) + 1 by XREAL_1:8;
then (2 * ((sqrt (n + 2)) * (sqrt (n + 1)))) + 1 < 2 * (n + 2) by SQUARE_1:29;
then (2 * ((sqrt (n + 2)) * (sqrt (n + 1)))) + 1 < 2 * (sqrt ((n + 2) ^2)) by SQUARE_1:22;
then ((2 * ((sqrt (n + 2)) * (sqrt (n + 1)))) + 1) / (sqrt (n + 2)) < (2 * (sqrt ((n + 2) * (n + 2)))) / (sqrt (n + 2)) by A3, XREAL_1:74;
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:29;
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 A3, XCMPLX_1:89;
then (((2 * (sqrt (n + 1))) * (sqrt (n + 2))) / (sqrt (n + 2))) + (1 / (sqrt (n + 2))) < 2 * (sqrt (n + 2)) by XCMPLX_1:62;
then A4: (2 * (sqrt (n + 1))) + (1 / (sqrt (n + 2))) < 2 * (sqrt (n + 2)) by A3, XCMPLX_1:89;
assume (Partial_Sums s) . n < 2 * (sqrt (n + 1)) ; :: thesis: S₁[n + 1]
then ((Partial_Sums s) . n) + (1 / (sqrt (n + 2))) < (2 * (sqrt (n + 1))) + (1 / (sqrt (n + 2))) by XREAL_1:8;
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;

(Partial_Sums s) . 0 = s . 0 by SERIES_1:def 1
.= 1 / (sqrt (0 + 1)) by A1
.= 1 ;
then A5: S₁[ 0 ] ;
for n being Nat holds S₁[n] from NAT_1:sch 2(A5, A2);
hence for n being Nat holds (Partial_Sums s) . n < 2 * (sqrt (n + 1)) ; :: thesis: verum