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

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) + 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 POWER:49;
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 A3: (1 - (1 / ((n + 2) * (n + 2)))) to_power ((n + 1) + 1) >= 1 - ((1 * 1) / (n + 2)) by XCMPLX_1:60;
(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)) by POWER:25
.= ((1 + (1 / (n + 1))) * ((1 + (1 / ((n + 1) + 1))) to_power ((n + 1) + 1))) / ((1 + (1 / (n + 1))) to_power ((n + 1) + 1)) by POWER:27
.= (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 POWER:31 ;
then (s . (n + 1)) / (s . n) >= (1 + (1 / (n + 1))) * (1 - (1 / (n + 2))) by A2, A3, 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 A4: (s . (n + 1)) / (s . n) >= 1 by XCMPLX_1:6, XCMPLX_1:60;
(1 + (1 / (n + 1))) to_power (n + 1) > 0 by POWER:34;
then s . n > 0 by A1;
hence s . (n + 1) >= s . n by A4, XREAL_1:191; :: thesis: verum

end;

hence s is non-decreasing ; :: thesis: verum