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

now

let n be Element of NAT ; :: thesis: s . (n + 1) >= s . n
A3: (1 + (1 / (n + 1))) to_power (n + 1) > 0 by Th39;
A4: (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:77
.= ((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)) by Th30
.= ((1 + (1 / (n + 1))) * ((1 + (1 / ((n + 1) + 1))) to_power ((n + 1) + 1))) / ((1 + (1 / (n + 1))) to_power ((n + 1) + 1)) by Th32
.= (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 Th36 ;
A5: (1 + (1 / ((n + 1) + 1))) / (1 + (1 / (n + 1))) = (((1 * ((n + 1) + 1)) + 1) / ((n + 1) + 1)) / (1 + (1 / (n + 1))) by XCMPLX_1:114
.= ((((n + 1) + 1) + 1) / ((n + 1) + 1)) / (((1 * (n + 1)) + 1) / (n + 1)) by XCMPLX_1:114
.= (((n + (1 + 1)) + 1) * (n + 1)) / ((n + 2) * (n + 2)) by XCMPLX_1:85
.= ((((((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:8;
then (n + 2) * (n + 2) > 1 by XREAL_1:163;
then 1 / ((n + 2) * (n + 2)) < 1 by XREAL_1:214;
then - (1 / ((n + 2) * (n + 2))) > - 1 by XREAL_1:26;
then (1 + (- (1 / ((n + 2) * (n + 2))))) to_power ((n + 1) + 1) >= 1 + (((n + 1) + 1) * (- (1 / ((n + 2) * (n + 2))))) by PREPOWER:24;
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:84;
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 A4, A5, XREAL_1:66;
then (s . (n + 1)) / (s . n) >= (((1 * (n + 1)) + 1) / (n + 1)) * (1 - (1 / (n + 2))) by XCMPLX_1:114;
then (s . (n + 1)) / (s . n) >= ((n + 2) / (n + 1)) * (((1 * (n + 2)) - 1) / (n + 2)) by XCMPLX_1:128;
then (s . (n + 1)) / (s . n) >= ((n + 1) * (n + 2)) / ((n + 1) * (n + 2)) by XCMPLX_1:77;
then A18: (s . (n + 1)) / (s . n) >= 1 by XCMPLX_1:6, XCMPLX_1:60;
s . n > 0 by A1, A3;
hence s . (n + 1) >= s . n by A18, XREAL_1:193; :: thesis: verum

end;

then A20: s is non-decreasing by SEQM_3:def 13;

now

let n be Element of NAT ; :: thesis: s . n < (2 * 2) + 1
A22: 2 * (n + 1) > 0 by XREAL_1:131;
A23: 2 * (n + 1) <> 0 ;
A24: 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 Th38 ;
(2 * (n + 1)) + 1 > 0 + 1 by A22, XREAL_1:8;
then 1 / ((2 * (n + 1)) + 1) < 1 by XREAL_1:214;
then A27: - (1 / ((2 * (n + 1)) + 1)) > - 1 by XREAL_1:26;
then A28: (- (1 / ((2 * (n + 1)) + 1))) + 1 > (- 1) + 1 by XREAL_1:8;
A29: (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 Th37
.= (1 / (((1 * (2 * (n + 1))) + 1) / (2 * (n + 1)))) to_power (- (n + 1)) by A23, XCMPLX_1:114
.= ((((2 * (n + 1)) + 1) - 1) / ((2 * (n + 1)) + 1)) to_power (- (n + 1)) by XCMPLX_1:78
.= ((((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 A28, Th33 ;
(1 + (- (1 / ((2 * (n + 1)) + 1)))) to_power (n + 1) >= 1 + ((n + 1) * (- (1 / ((2 * (n + 1)) + 1)))) by A27, PREPOWER:24;
then (1 - (1 / ((2 * (n + 1)) + 1))) to_power (n + 1) >= 1 - ((n + 1) / ((2 * (n + 1)) + 1)) ;
then A32: (1 - (1 / ((2 * (n + 1)) + 1))) to_power (n + 1) >= ((1 * ((2 * (n + 1)) + 1)) - (n + 1)) / ((2 * (n + 1)) + 1) by XCMPLX_1:128;

now

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:104;
then (2 * (n + 1)) + ((- n) + ((2 * (n + 1)) - n)) < (2 * (n + 1)) + 1 ;
hence contradiction by XREAL_1:8; :: thesis: verum

end;

then (1 - (1 / ((2 * (n + 1)) + 1))) to_power (n + 1) >= 1 / 2 by A32, XXREAL_0:2;
then A38: (1 + (1 / (2 * (n + 1)))) to_power (n + 1) <= 1 / (1 / 2) by A29, XREAL_1:87;
(1 + (1 / (2 * (n + 1)))) to_power (n + 1) > 0 by Th39;
then ((1 + (1 / (2 * (n + 1)))) to_power (n + 1)) ^2 <= 2 * 2 by A38, XREAL_1:68;
then A41: s . (n + (n + 1)) <= 2 * 2 by A24, Th53;
s . n <= s . (n + (n + 1)) by A20, SEQM_3:11;
then s . n <= 2 * 2 by A41, 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 A20; :: thesis: verum