set s2 = seq_const 1;
let s be Real_Sequence; :: thesis:
let a be Real; :: thesis:
assume A1: a >= 1 ; :: thesis:
deffunc H₁( Nat) -> set = (a - 1) / ($1 + 1);
consider s1 being Real_Sequence such that
A2: for n being Nat holds s1 . n = H₁(n) from SEQ_1:sch 1();
set s3 = (seq_const 1) + s1;
A3: s1 is convergent by A2, SEQ_4:31;
then A4: (seq_const 1) + s1 is convergent ;
assume A5: for n being Nat st n >= 1 holds
s . n = n -Root a ; :: thesis:

let n be Nat; :: thesis:
A7: n + 1 >= 0 + 1 by XREAL_1:6;
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, Th29;
then ((s ^\ 1) . n) - 1 >= 0 by XREAL_1:48;
then A10: - 1 < ((s ^\ 1) . n) - 1 ;
a = (1 + (((s ^\ 1) . n) - 1)) |^ (n + 1) by A1, A7, A8, Lm2;
then a >= 1 + ((n + 1) * (((s ^\ 1) . n) - 1)) by A10, Th16;
then a - 1 >= (1 + ((n + 1) * (((s ^\ 1) . n) - 1))) - 1 by XREAL_1:9;
then (a - 1) * ((n + 1) ") >= ((n + 1) ") * ((n + 1) * (((s ^\ 1) . n) - 1)) by XREAL_1:64;
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:6;
then ((seq_const 1) . n) + ((a - 1) / (n + 1)) >= (s ^\ 1) . n by SEQ_1:57;
then ((seq_const 1) . n) + (s1 . n) >= (s ^\ 1) . n by A2;
hence ( (seq_const 1) . n <= (s ^\ 1) . n & (s ^\ 1) . n <= ((seq_const 1) + s1) . n ) by A9, SEQ_1:57, SEQ_1:7; :: thesis:

end;