let a be Real; :: thesis: for s being Real_Sequence st a > 0 & ( for n being Nat st n >= 1 holds

s . n = n -Root a ) holds

( s is convergent & lim s = 1 )

let s be Real_Sequence; :: thesis: ( a > 0 & ( for n being Nat st n >= 1 holds

s . n = n -Root a ) implies ( s is convergent & lim s = 1 ) )

assume A1: a > 0 ; :: thesis: ( ex n being Nat st

( n >= 1 & not s . n = n -Root a ) or ( s is convergent & lim s = 1 ) )

assume A2: for n being Nat st n >= 1 holds

s . n = n -Root a ; :: thesis: ( s is convergent & lim s = 1 )

s . n = n -Root a ) holds

( s is convergent & lim s = 1 )

let s be Real_Sequence; :: thesis: ( a > 0 & ( for n being Nat st n >= 1 holds

s . n = n -Root a ) implies ( s is convergent & lim s = 1 ) )

assume A1: a > 0 ; :: thesis: ( ex n being Nat st

( n >= 1 & not s . n = n -Root a ) or ( s is convergent & lim s = 1 ) )

assume A2: for n being Nat st n >= 1 holds

s . n = n -Root a ; :: thesis: ( s is convergent & lim s = 1 )

per cases
( a >= 1 or a < 1 )
;

end;

suppose A3:
a < 1
; :: thesis: ( s is convergent & lim s = 1 )

then
a / a < 1 / a
by A1, XREAL_1:74;

then A4: 1 <= 1 / a by A1, XCMPLX_1:60;

deffunc H_{1}( Nat) -> Real = $1 -Root (1 / a);

consider s1 being Real_Sequence such that

A5: for n being Nat holds s1 . n = H_{1}(n)
from SEQ_1:sch 1();

A6: for n being Nat st n >= 1 holds

s1 . n = n -Root (1 / a) by A5;

then A7: lim s1 = 1 by A4, Lm3;

A8: s1 is convergent by A4, A6, Lm3;

hence lim s = 1 by A9, SEQ_2:def 7; :: thesis: verum

end;then A4: 1 <= 1 / a by A1, XCMPLX_1:60;

deffunc H

consider s1 being Real_Sequence such that

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

A6: for n being Nat st n >= 1 holds

s1 . n = n -Root (1 / a) by A5;

then A7: lim s1 = 1 by A4, Lm3;

A8: s1 is convergent by A4, A6, Lm3;

A9: now :: thesis: for b being Real st b > 0 holds

ex n being Nat st

for m being Nat st n <= m holds

|.((s . m) - 1).| < b

hence
s is convergent
by SEQ_2:def 6; :: thesis: lim s = 1ex n being Nat st

for m being Nat st n <= m holds

|.((s . m) - 1).| < b

let b be Real; :: thesis: ( b > 0 implies ex n being Nat st

for m being Nat st n <= m holds

|.((s . m) - 1).| < b )

assume b > 0 ; :: thesis: ex n being Nat st

for m being Nat st n <= m holds

|.((s . m) - 1).| < b

then consider m1 being Nat such that

A10: for m being Nat st m1 <= m holds

|.((s1 . m) - 1).| < b by A8, A7, SEQ_2:def 7;

reconsider n = m1 + 1 as Nat ;

take n = n; :: thesis: for m being Nat st n <= m holds

|.((s . m) - 1).| < b

let m be Nat; :: thesis: ( n <= m implies |.((s . m) - 1).| < b )

assume A11: n <= m ; :: thesis: |.((s . m) - 1).| < b

A12: n >= 0 + 1 by XREAL_1:6;

then A13: 1 <= m by A11, XXREAL_0:2;

then A14: m -Root a < 1 by A1, A3, Th30;

A15: m -Root a <> 0 by A1, A13, Def2;

then A16: |.((1 / (m -Root a)) - 1).| = |.((1 / (m -Root a)) - ((m -Root a) / (m -Root a))).| by XCMPLX_1:60

.= |.((1 - (m -Root a)) / (m -Root a)).|

.= |.((1 - (m -Root a)) * ((m -Root a) ")).|

.= |.(1 - (m -Root a)).| * |.((m -Root a) ").| by COMPLEX1:65 ;

0 < m -Root a by A1, A3, A13, Th30;

then (m -Root a) * ((m -Root a) ") < 1 * ((m -Root a) ") by A14, XREAL_1:68;

then 1 < (m -Root a) " by A15, XCMPLX_0:def 7;

then A17: 1 < |.((m -Root a) ").| by ABSVALUE:def 1;

0 <> 1 - (m -Root a) by A1, A3, A13, Th30;

then |.(1 - (m -Root a)).| > 0 by COMPLEX1:47;

then A18: 1 * |.(1 - (m -Root a)).| < |.(1 - (m -Root a)).| * |.((m -Root a) ").| by A17, XREAL_1:68;

m1 <= n by XREAL_1:29;

then m1 <= m by A11, XXREAL_0:2;

then |.((s1 . m) - 1).| < b by A10;

then |.((m -Root (1 / a)) - 1).| < b by A5;

then |.((1 / (m -Root a)) - 1).| < b by A1, A13, Th23;

then |.(- ((m -Root a) - 1)).| < b by A16, A18, XXREAL_0:2;

then |.((m -Root a) - 1).| < b by COMPLEX1:52;

hence |.((s . m) - 1).| < b by A2, A12, A11, XXREAL_0:2; :: thesis: verum

end;for m being Nat st n <= m holds

|.((s . m) - 1).| < b )

assume b > 0 ; :: thesis: ex n being Nat st

for m being Nat st n <= m holds

|.((s . m) - 1).| < b

then consider m1 being Nat such that

A10: for m being Nat st m1 <= m holds

|.((s1 . m) - 1).| < b by A8, A7, SEQ_2:def 7;

reconsider n = m1 + 1 as Nat ;

take n = n; :: thesis: for m being Nat st n <= m holds

|.((s . m) - 1).| < b

let m be Nat; :: thesis: ( n <= m implies |.((s . m) - 1).| < b )

assume A11: n <= m ; :: thesis: |.((s . m) - 1).| < b

A12: n >= 0 + 1 by XREAL_1:6;

then A13: 1 <= m by A11, XXREAL_0:2;

then A14: m -Root a < 1 by A1, A3, Th30;

A15: m -Root a <> 0 by A1, A13, Def2;

then A16: |.((1 / (m -Root a)) - 1).| = |.((1 / (m -Root a)) - ((m -Root a) / (m -Root a))).| by XCMPLX_1:60

.= |.((1 - (m -Root a)) / (m -Root a)).|

.= |.((1 - (m -Root a)) * ((m -Root a) ")).|

.= |.(1 - (m -Root a)).| * |.((m -Root a) ").| by COMPLEX1:65 ;

0 < m -Root a by A1, A3, A13, Th30;

then (m -Root a) * ((m -Root a) ") < 1 * ((m -Root a) ") by A14, XREAL_1:68;

then 1 < (m -Root a) " by A15, XCMPLX_0:def 7;

then A17: 1 < |.((m -Root a) ").| by ABSVALUE:def 1;

0 <> 1 - (m -Root a) by A1, A3, A13, Th30;

then |.(1 - (m -Root a)).| > 0 by COMPLEX1:47;

then A18: 1 * |.(1 - (m -Root a)).| < |.(1 - (m -Root a)).| * |.((m -Root a) ").| by A17, XREAL_1:68;

m1 <= n by XREAL_1:29;

then m1 <= m by A11, XXREAL_0:2;

then |.((s1 . m) - 1).| < b by A10;

then |.((m -Root (1 / a)) - 1).| < b by A5;

then |.((1 / (m -Root a)) - 1).| < b by A1, A13, Th23;

then |.(- ((m -Root a) - 1)).| < b by A16, A18, XXREAL_0:2;

then |.((m -Root a) - 1).| < b by COMPLEX1:52;

hence |.((s . m) - 1).| < b by A2, A12, A11, XXREAL_0:2; :: thesis: verum

hence lim s = 1 by A9, SEQ_2:def 7; :: thesis: verum