set s2 = seq_const 1;
let s be Real_Sequence; :: thesis: for a being Real st a >= 1 & ( for n being Nat st n >= 1 holds
s . n = n -Root a ) holds
( s is convergent & lim s = 1 )

let a be Real; :: thesis: ( a >= 1 & ( for n being Nat st n >= 1 holds
s . n = n -Root a ) implies ( s is convergent & lim s = 1 ) )

assume A1: a >= 1 ; :: thesis: ( ex n being Nat st
( n >= 1 & not s . n = n -Root a ) or ( s is convergent & lim s = 1 ) )

deffunc H1( Nat) -> set = (a - 1) / (\$1 + 1);
consider s1 being Real_Sequence such that
A2: for n being Nat holds s1 . n = H1(n) from SEQ_1:sch 1();
set s3 = () + s1;
A3: s1 is convergent by ;
then A4: (seq_const 1) + s1 is convergent ;
assume A5: for n being Nat st n >= 1 holds
s . n = n -Root a ; :: thesis: ( s is convergent & lim s = 1 )
A6: now :: thesis: for n being Nat holds
( () . n <= (s ^\ 1) . n & (s ^\ 1) . n <= (() + s1) . n )
let n be Nat; :: thesis: ( () . n <= (s ^\ 1) . n & (s ^\ 1) . n <= (() + s1) . n )
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 ;
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 <= (() + s1) . n ) by ; :: thesis: verum
end;
lim s1 = 0 by ;
then A11: lim (() + s1) = (() . 0) + 0 by
.= 1 by SEQ_1:57 ;
A12: lim () = () . 0 by SEQ_4:26
.= 1 by SEQ_1:57 ;
then A13: s ^\ 1 is convergent by ;
hence s is convergent by SEQ_4:21; :: thesis: lim s = 1
lim (s ^\ 1) = 1 by ;
hence lim s = 1 by ; :: thesis: verum