let s be Real_Sequence; :: thesis: ( ( for n being Nat holds s . n = (1 + (1 / (n + 1))) to_power (n + 1) ) implies s is convergent )
assume A1: for n being Nat holds s . n = (1 + (1 / (n + 1))) to_power (n + 1) ; :: thesis: s is convergent

now :: thesis: for n being Nat holds s . (n + 1) >= s . n

let n be Nat; :: thesis: s . (n + 1) >= s . n
A2: (1 + (1 / (n + 1))) to_power (n + 1) > 0 by Th34;
A3: (s . (n + 1)) / (s . n) = ((1 + (1 / ((n + 1) + 1))) to_power ((n + 1) + 1)) / (s . n) by A1
.= (((1 + (1 / ((n + 1) + 1))) to_power ((n + 1) + 1)) / ((1 + (1 / (n + 1))) to_power (n + 1))) * 1 by A1
.= (((1 + (1 / ((n + 1) + 1))) to_power ((n + 1) + 1)) / ((1 + (1 / (n + 1))) to_power (n + 1))) * ((1 + (1 / (n + 1))) / (1 + (1 / (n + 1)))) by XCMPLX_1:60
.= ((1 + (1 / (n + 1))) * ((1 + (1 / ((n + 1) + 1))) to_power ((n + 1) + 1))) / (((1 + (1 / (n + 1))) to_power (n + 1)) * (1 + (1 / (n + 1)))) by XCMPLX_1:76
.= ((1 + (1 / (n + 1))) * ((1 + (1 / ((n + 1) + 1))) to_power ((n + 1) + 1))) / (((1 + (1 / (n + 1))) to_power (n + 1)) * ((1 + (1 / (n + 1))) to_power 1))
.= ((1 + (1 / (n + 1))) * ((1 + (1 / ((n + 1) + 1))) to_power ((n + 1) + 1))) / ((1 + (1 / (n + 1))) to_power ((n + 1) + 1)) by Th27
.= (1 + (1 / (n + 1))) * (((1 + (1 / ((n + 1) + 1))) to_power ((n + 1) + 1)) / ((1 + (1 / (n + 1))) to_power ((n + 1) + 1)))
.= (1 + (1 / (n + 1))) * (((1 + (1 / ((n + 1) + 1))) / (1 + (1 / (n + 1)))) to_power ((n + 1) + 1)) by Th31 ;
A4: (1 + (1 / ((n + 1) + 1))) / (1 + (1 / (n + 1))) = (((1 * ((n + 1) + 1)) + 1) / ((n + 1) + 1)) / (1 + (1 / (n + 1))) by XCMPLX_1:113
.= ((((n + 1) + 1) + 1) / ((n + 1) + 1)) / (((1 * (n + 1)) + 1) / (n + 1)) by XCMPLX_1:113
.= (((n + (1 + 1)) + 1) * (n + 1)) / ((n + 2) * (n + 2)) by XCMPLX_1:84
.= ((((((n * n) + (n * 2)) + (2 * n)) + 3) + 1) - 1) / ((n + 2) * (n + 2))
.= (((n + 2) * (n + 2)) / ((n + 2) * (n + 2))) - (1 / ((n + 2) * (n + 2)))
.= 1 - (1 / ((n + 2) * (n + 2))) by XCMPLX_1:6, XCMPLX_1:60 ;
(n + 1) + 1 > 0 + 1 by XREAL_1:6;
then (n + 2) * (n + 2) > 1 by XREAL_1:161;
then 1 / ((n + 2) * (n + 2)) < 1 by XREAL_1:212;
then - (1 / ((n + 2) * (n + 2))) > - 1 by XREAL_1:24;
then (1 + (- (1 / ((n + 2) * (n + 2))))) to_power ((n + 1) + 1) >= 1 + (((n + 1) + 1) * (- (1 / ((n + 2) * (n + 2))))) by PREPOWER:16;
then (1 - (1 / ((n + 2) * (n + 2)))) to_power ((n + 1) + 1) >= 1 - (((n + 2) * 1) / ((n + 2) * (n + 2))) ;
then (1 - (1 / ((n + 2) * (n + 2)))) to_power ((n + 1) + 1) >= 1 - ((((n + 2) / (n + 2)) * 1) / (n + 2)) by XCMPLX_1:83;
then (1 - (1 / ((n + 2) * (n + 2)))) to_power ((n + 1) + 1) >= 1 - ((1 * 1) / (n + 2)) by XCMPLX_1:60;
then (s . (n + 1)) / (s . n) >= (1 + (1 / (n + 1))) * (1 - (1 / (n + 2))) by A3, A4, XREAL_1:64;
then (s . (n + 1)) / (s . n) >= (((1 * (n + 1)) + 1) / (n + 1)) * (1 - (1 / (n + 2))) by XCMPLX_1:113;
then (s . (n + 1)) / (s . n) >= ((n + 2) / (n + 1)) * (((1 * (n + 2)) - 1) / (n + 2)) by XCMPLX_1:127;
then (s . (n + 1)) / (s . n) >= ((n + 1) * (n + 2)) / ((n + 1) * (n + 2)) by XCMPLX_1:76;
then A5: (s . (n + 1)) / (s . n) >= 1 by XCMPLX_1:6, XCMPLX_1:60;
s . n > 0 by A1, A2;
hence s . (n + 1) >= s . n by A5, XREAL_1:191; :: thesis: verum

end;

then A6: s is non-decreasing by SEQM_3:def 8;

now :: thesis: for n being Nat holds s . n < (2 * 2) + 1

let n be Nat; :: thesis: s . n < (2 * 2) + 1
A7: 2 * (n + 1) > 0 by XREAL_1:129;
A8: 2 * (n + 1) <> 0 ;
A9: s . (n + (n + 1)) = (1 + (1 / ((2 * n) + (1 + 1)))) to_power (((2 * n) + 1) + 1) by A1
.= ((1 + (1 / (2 * (n + 1)))) to_power (n + 1)) to_power 2 by Th33 ;
(2 * (n + 1)) + 1 > 0 + 1 by A7, XREAL_1:6;
then 1 / ((2 * (n + 1)) + 1) < 1 by XREAL_1:212;
then A10: - (1 / ((2 * (n + 1)) + 1)) > - 1 by XREAL_1:24;
then A11: (- (1 / ((2 * (n + 1)) + 1))) + 1 > (- 1) + 1 by XREAL_1:6;
A12: (1 + (1 / (2 * (n + 1)))) to_power (n + 1) = (1 / (1 / (1 + (1 / (2 * (n + 1)))))) to_power (n + 1)
.= (1 / (1 + (1 / (2 * (n + 1))))) to_power (- (n + 1)) by Th32
.= (1 / (((1 * (2 * (n + 1))) + 1) / (2 * (n + 1)))) to_power (- (n + 1)) by A8, XCMPLX_1:113
.= ((((2 * (n + 1)) + 1) - 1) / ((2 * (n + 1)) + 1)) to_power (- (n + 1)) by XCMPLX_1:77
.= ((((2 * (n + 1)) + 1) / ((2 * (n + 1)) + 1)) - (1 / ((2 * (n + 1)) + 1))) to_power (- (n + 1))
.= (1 - (1 / ((2 * (n + 1)) + 1))) to_power (- (n + 1)) by XCMPLX_1:60
.= 1 / ((1 - (1 / ((2 * (n + 1)) + 1))) to_power (n + 1)) by A11, Th28 ;
(1 + (- (1 / ((2 * (n + 1)) + 1)))) to_power (n + 1) >= 1 + ((n + 1) * (- (1 / ((2 * (n + 1)) + 1)))) by A10, PREPOWER:16;
then (1 - (1 / ((2 * (n + 1)) + 1))) to_power (n + 1) >= 1 - ((n + 1) / ((2 * (n + 1)) + 1)) ;
then A13: (1 - (1 / ((2 * (n + 1)) + 1))) to_power (n + 1) >= ((1 * ((2 * (n + 1)) + 1)) - (n + 1)) / ((2 * (n + 1)) + 1) by XCMPLX_1:127;

now :: thesis: not ((2 * (n + 1)) - n) / ((2 * (n + 1)) + 1) < 1 / 2

assume ((2 * (n + 1)) - n) / ((2 * (n + 1)) + 1) < 1 / 2 ; :: thesis: contradiction
then ((2 * (n + 1)) - n) * 2 < ((2 * (n + 1)) + 1) * 1 by XREAL_1:102;
then (2 * (n + 1)) + ((- n) + ((2 * (n + 1)) - n)) < (2 * (n + 1)) + 1 ;
hence contradiction by XREAL_1:6; :: thesis: verum

end;

then (1 - (1 / ((2 * (n + 1)) + 1))) to_power (n + 1) >= 1 / 2 by A13, XXREAL_0:2;
then A14: (1 + (1 / (2 * (n + 1)))) to_power (n + 1) <= 1 / (1 / 2) by A12, XREAL_1:85;
(1 + (1 / (2 * (n + 1)))) to_power (n + 1) > 0 by Th34;
then ((1 + (1 / (2 * (n + 1)))) to_power (n + 1)) ^2 <= 2 * 2 by A14, XREAL_1:66;
then A15: s . (n + (n + 1)) <= 2 * 2 by A9, Th46;
s . n <= s . (n + (n + 1)) by A6, SEQM_3:5;
then s . n <= 2 * 2 by A15, XXREAL_0:2;
hence s . n < (2 * 2) + 1 by XXREAL_0:2; :: thesis: verum

end;

then s is bounded_above by SEQ_2:def 3;
hence s is convergent by A6; :: thesis: verum