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 H_{1}( Nat) -> set = (a - 1) / ($1 + 1);

consider s1 being Real_Sequence such that

A2: for n being Nat holds s1 . n = H_{1}(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: ( s is convergent & lim s = 1 )

then A11: lim ((seq_const 1) + s1) = ((seq_const 1) . 0) + 0 by A3, SEQ_4:42

.= 1 by SEQ_1:57 ;

A12: lim (seq_const 1) = (seq_const 1) . 0 by SEQ_4:26

.= 1 by SEQ_1:57 ;

then A13: s ^\ 1 is convergent by A4, A11, A6, SEQ_2:19;

hence s is convergent by SEQ_4:21; :: thesis: lim s = 1

lim (s ^\ 1) = 1 by A4, A11, A12, A6, SEQ_2:20;

hence lim s = 1 by A13, SEQ_4:22; :: thesis: verum

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 H

consider s1 being Real_Sequence such that

A2: for n being Nat holds s1 . n = H

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: ( s is convergent & lim s = 1 )

A6: now :: thesis: for n being Nat holds

( (seq_const 1) . n <= (s ^\ 1) . n & (s ^\ 1) . n <= ((seq_const 1) + s1) . n )

lim s1 = 0
by A2, SEQ_4:31;( (seq_const 1) . n <= (s ^\ 1) . n & (s ^\ 1) . n <= ((seq_const 1) + s1) . n )

let n be Nat; :: thesis: ( (seq_const 1) . n <= (s ^\ 1) . n & (s ^\ 1) . n <= ((seq_const 1) + 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 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: verum

end;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: verum

then A11: lim ((seq_const 1) + s1) = ((seq_const 1) . 0) + 0 by A3, SEQ_4:42

.= 1 by SEQ_1:57 ;

A12: lim (seq_const 1) = (seq_const 1) . 0 by SEQ_4:26

.= 1 by SEQ_1:57 ;

then A13: s ^\ 1 is convergent by A4, A11, A6, SEQ_2:19;

hence s is convergent by SEQ_4:21; :: thesis: lim s = 1

lim (s ^\ 1) = 1 by A4, A11, A12, A6, SEQ_2:20;

hence lim s = 1 by A13, SEQ_4:22; :: thesis: verum