reconsider s2 = NAT --> 1 as Real_Sequence by FUNCOP_1:57;
let s be Real_Sequence; :: thesis:
let a be real number ; :: thesis:
assume A1: a >= 1 ; :: thesis:
deffunc H₁( Element of NAT ) -> Element of REAL = (a - 1) / ($1 + 1);
consider s1 being Real_Sequence such that
A2: for n being Element of NAT holds s1 . n = H₁(n) from SEQ_1:sch 1();
set s3 = s2 + s1;
A3: s1 is convergent by A2, SEQ_4:46;
then A4: s2 + s1 is convergent by SEQ_2:19;
assume A5: for n being Element of NAT st n >= 1 holds
s . n = n -Root a ; :: thesis:

let n be Element of NAT ; :: thesis:
A7: n + 1 >= 0 + 1 by XREAL_1:8;
set b = ((s ^\ 1) . n) - 1;
A8: (s ^\ 1) . n = s . (n + 1) by NAT_1:def 3
.= (n + 1) -Root a by A5, A7 ;
then A9: (s ^\ 1) . n >= 1 by A1, A7, Th38;
then ((s ^\ 1) . n) - 1 >= 0 by XREAL_1:50;
then A10: - 1 < ((s ^\ 1) . n) - 1 by XXREAL_0:2;
a = (1 + (((s ^\ 1) . n) - 1)) |^ (n + 1) by A1, A7, A8, Lm2;
then a >= 1 + ((n + 1) * (((s ^\ 1) . n) - 1)) by A10, Th24;
then a - 1 >= (1 + ((n + 1) * (((s ^\ 1) . n) - 1))) - 1 by XREAL_1:11;
then (a - 1) * ((n + 1) " ) >= ((n + 1) " ) * ((n + 1) * (((s ^\ 1) . n) - 1)) by XREAL_1:66;
then (a - 1) * ((n + 1) " ) >= (((n + 1) " ) * (n + 1)) * (((s ^\ 1) . n) - 1) ;
then (a - 1) * ((n + 1) " ) >= 1 * (((s ^\ 1) . n) - 1) by XCMPLX_0:def 7;
then ((a - 1) / (n + 1)) + 1 >= (((s ^\ 1) . n) - 1) + 1 by XREAL_1:8;
then (s2 . n) + ((a - 1) / (n + 1)) >= (s ^\ 1) . n by FUNCOP_1:13;
then (s2 . n) + (s1 . n) >= (s ^\ 1) . n by A2;
hence ( s2 . n <= (s ^\ 1) . n & (s ^\ 1) . n <= (s2 + s1) . n ) by A9, FUNCOP_1:13, SEQ_1:11; :: thesis:

end;