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:76;
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();
for n being Element of NAT st n >= 1 holds
s1 . n = n -Root (1 / a) by A5;
then A6: ( s1 is convergent & lim s1 = 1 ) by A4, Lm3;

A7: 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
A8: for m being Element of NAT st m1 <= m holds
abs ((s1 . m) - 1) < b by A6, SEQ_2:def 7;
take n = m1 + 1; :: thesis: for m being Element of NAT st n <= m holds
abs ((s . m) - 1) < b
A9: n >= 0 + 1 by XREAL_1:8;
let m be Element of NAT ; :: thesis: ( n <= m implies abs ((s . m) - 1) < b )
assume A10: n <= m ; :: thesis: abs ((s . m) - 1) < b
then A11: 1 <= m by A9, XXREAL_0:2;
m1 <= n by XREAL_1:31;
then m1 <= m by A10, XXREAL_0:2;
then abs ((s1 . m) - 1) < b by A8;
then abs ((m -Root (1 / a)) - 1) < b by A5;
then A12: abs ((1 / (m -Root a)) - 1) < b by A1, A11, Th32;
A13: m -Root a <> 0 by A1, A11, Def3;
then A14: 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:151 ;
( 0 < m -Root a & m -Root a < 1 ) by A1, A3, A11, Th39;
then ( 0 < (m -Root a) " & m -Root a < 1 ) ;
then (m -Root a) * ((m -Root a) " ) < 1 * ((m -Root a) " ) by XREAL_1:70;
then 1 < (m -Root a) " by A13, XCMPLX_0:def 7;
then A15: 1 < abs ((m -Root a) " ) by ABSVALUE:def 1;
0 <> 1 - (m -Root a) by A1, A3, A11, Th39;
then abs (1 - (m -Root a)) > 0 by COMPLEX1:133;
then 1 * (abs (1 - (m -Root a))) < (abs (1 - (m -Root a))) * (abs ((m -Root a) " )) by A15, XREAL_1:70;
then abs (- ((m -Root a) - 1)) < b by A12, A14, XXREAL_0:2;
then abs ((m -Root a) - 1) < b by COMPLEX1:138;
hence abs ((s . m) - 1) < b by A2, A9, A10, XXREAL_0:2; :: thesis: verum

end;

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

end;

end;