let a be real number ; :: thesis: for s being Real_Sequence st a > 0 & ( for n being Element of 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 Element of 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 Element of NAT st
( n >= 1 & not s . n = n -Root a ) or ( s is convergent & lim s = 1 ) )
assume A2: for n being Element of NAT st n >= 1 holds
s . n = n -Root a ; :: thesis: ( s is convergent & lim s = 1 )

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

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

hence ( s is convergent & lim s = 1 ) by A2, Lm3; :: thesis: verum

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₁( Element of NAT ) -> Real = $1 -Root (1 / a);
consider s1 being Real_Sequence such that
A5: for n being Element of NAT holds s1 . n = H₁(n) from SEQ_1:sch 1();
A6: for n being Element of 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

let b be real number ; :: thesis: ( b > 0 implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((s . m) - 1) < b )
assume b > 0 ; :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((s . m) - 1) < b
then consider m1 being Element of NAT such that
A10: for m being Element of NAT st m1 <= m holds
abs ((s1 . m) - 1) < b by A8, A7, SEQ_2:def 7;
take n = m1 + 1; :: thesis: for m being Element of NAT st n <= m holds
abs ((s . m) - 1) < b
let m be Element of NAT ; :: thesis: ( n <= m implies abs ((s . m) - 1) < b )
assume A11: n <= m ; :: thesis: abs ((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, Th39;
A15: m -Root a <> 0 by A1, A13, Def3;
then A16: abs ((1 / (m -Root a)) - 1) = abs ((1 / (m -Root a)) - ((m -Root a) / (m -Root a))) by XCMPLX_1:60
.= abs ((1 - (m -Root a)) / (m -Root a))
.= abs ((1 - (m -Root a)) * ((m -Root a) "))
.= (abs (1 - (m -Root a))) * (abs ((m -Root a) ")) by COMPLEX1:65 ;
0 < m -Root a by A1, A3, A13, Th39;
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 < abs ((m -Root a) ") by ABSVALUE:def 1;
0 <> 1 - (m -Root a) by A1, A3, A13, Th39;
then abs (1 - (m -Root a)) > 0 by COMPLEX1:47;
then A18: 1 * (abs (1 - (m -Root a))) < (abs (1 - (m -Root a))) * (abs ((m -Root a) ")) by A17, XREAL_1:68;
m1 <= n by XREAL_1:29;
then m1 <= m by A11, XXREAL_0:2;
then abs ((s1 . m) - 1) < b by A10;
then abs ((m -Root (1 / a)) - 1) < b by A5;
then abs ((1 / (m -Root a)) - 1) < b by A1, A13, Th32;
then abs (- ((m -Root a) - 1)) < b by A16, A18, XXREAL_0:2;
then abs ((m -Root a) - 1) < b by COMPLEX1:52;
hence abs ((s . m) - 1) < b by A2, A12, A11, XXREAL_0:2; :: thesis: verum

end;

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

end;

end;