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

A2: 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 ;
A6: (n + 1) + 1 > 0 + 1 by XREAL_1:8;
A7: (n + 2) * (n + 2) > 1 by A6, XREAL_1:163;
A8: 1 / ((n + 2) * (n + 2)) < 1 by A7, XREAL_1:214;
A9: - (1 / ((n + 2) * (n + 2))) > - 1 by A8, XREAL_1:26;
A10: (1 + (- (1 / ((n + 2) * (n + 2))))) to_power ((n + 1) + 1) >= 1 + (((n + 1) + 1) * (- (1 / ((n + 2) * (n + 2))))) by A9, PREPOWER:24;
A11: (1 - (1 / ((n + 2) * (n + 2)))) to_power ((n + 1) + 1) >= 1 - (((n + 2) * 1) / ((n + 2) * (n + 2))) by A10;
A12: (1 - (1 / ((n + 2) * (n + 2)))) to_power ((n + 1) + 1) >= 1 - ((((n + 2) / (n + 2)) * 1) / (n + 2)) by A11, XCMPLX_1:84;
A13: (1 - (1 / ((n + 2) * (n + 2)))) to_power ((n + 1) + 1) >= 1 - ((1 * 1) / (n + 2)) by A12, XCMPLX_1:60;
A14: (s . (n + 1)) / (s . n) >= (1 + (1 / (n + 1))) * (1 - (1 / (n + 2))) by A4, A5, A13, XREAL_1:66;
A15: (s . (n + 1)) / (s . n) >= (((1 * (n + 1)) + 1) / (n + 1)) * (1 - (1 / (n + 2))) by A14, XCMPLX_1:114;
A16: (s . (n + 1)) / (s . n) >= ((n + 2) / (n + 1)) * (((1 * (n + 2)) - 1) / (n + 2)) by A15, XCMPLX_1:128;
A17: (s . (n + 1)) / (s . n) >= ((n + 1) * (n + 2)) / ((n + 1) * (n + 2)) by A16, XCMPLX_1:77;
A18: (s . (n + 1)) / (s . n) >= 1 by A17, XCMPLX_1:6, XCMPLX_1:60;
A19: s . n > 0 by A1, A3;
thus s . (n + 1) >= s . n by A18, A19, XREAL_1:193; :: thesis: verum

end;

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

A21: 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 ;
A25: (2 * (n + 1)) + 1 > 0 + 1 by A22, XREAL_1:8;
A26: 1 / ((2 * (n + 1)) + 1) < 1 by A25, XREAL_1:214;
A27: - (1 / ((2 * (n + 1)) + 1)) > - 1 by A26, XREAL_1:26;
A28: (- (1 / ((2 * (n + 1)) + 1))) + 1 > (- 1) + 1 by A27, 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 ;
A30: (1 + (- (1 / ((2 * (n + 1)) + 1)))) to_power (n + 1) >= 1 + ((n + 1) * (- (1 / ((2 * (n + 1)) + 1)))) by A27, PREPOWER:24;
A31: (1 - (1 / ((2 * (n + 1)) + 1))) to_power (n + 1) >= 1 - ((n + 1) / ((2 * (n + 1)) + 1)) by A30;
A32: (1 - (1 / ((2 * (n + 1)) + 1))) to_power (n + 1) >= ((1 * ((2 * (n + 1)) + 1)) - (n + 1)) / ((2 * (n + 1)) + 1) by A31, XCMPLX_1:128;

A33: now

assume A34: ((2 * (n + 1)) - n) / ((2 * (n + 1)) + 1) < 1 / 2 ; :: thesis: contradiction
A35: ((2 * (n + 1)) - n) * 2 < ((2 * (n + 1)) + 1) * 1 by A34, XREAL_1:104;
A36: (2 * (n + 1)) + ((- n) + ((2 * (n + 1)) - n)) < (2 * (n + 1)) + 1 by A35;
thus contradiction by A36, XREAL_1:8; :: thesis: verum

end;

A37: (1 - (1 / ((2 * (n + 1)) + 1))) to_power (n + 1) >= 1 / 2 by A32, A33, XXREAL_0:2;
A38: (1 + (1 / (2 * (n + 1)))) to_power (n + 1) <= 1 / (1 / 2) by A29, A37, XREAL_1:87;
A39: (1 + (1 / (2 * (n + 1)))) to_power (n + 1) > 0 by Th39;
A40: ((1 + (1 / (2 * (n + 1)))) to_power (n + 1)) ^2 <= 2 * 2 by A38, A39, XREAL_1:68;
A41: s . (n + (n + 1)) <= 2 * 2 by A24, A40, Th53;
A42: s . n <= s . (n + (n + 1)) by A20, SEQM_3:11;
A43: s . n <= 2 * 2 by A41, A42, XXREAL_0:2;
thus s . n < (2 * 2) + 1 by A43, XXREAL_0:2; :: thesis: verum

end;

A44: s is bounded_above by A21, SEQ_2:def 3;
thus s is convergent by A20, A44; :: thesis: verum