let a be real number ; :: thesis: for s being Real_Sequence st abs a < 1 & ( for n being Element of NAT holds s . n = a to_power (n + 1) ) holds
( s is convergent & lim s = 0 )
let s be Real_Sequence; :: thesis: ( abs a < 1 & ( for n being Element of NAT holds s . n = a to_power (n + 1) ) implies ( s is convergent & lim s = 0 ) )
assume that
A1: abs a < 1 and
A2: for n being Element of NAT holds s . n = a to_power (n + 1) ; :: thesis: ( s is convergent & lim s = 0 )

now

per cases ( abs a = 0 or not abs a = 0 ) ;

suppose abs a = 0 ; :: thesis: ( s is convergent & lim s = 0 )

then A3: a = 0 by ABSVALUE:2;

now

let n be Nat; :: thesis: s . n = 0
( n in NAT & a to_power (n + 1) = 0 ) by A3, ORDINAL1:def 12, POWER:def 2;
hence s . n = 0 by A2; :: thesis: verum

end;

then ( s is constant & s . 0 = 0 ) by VALUED_0:def 18;
hence ( s is convergent & lim s = 0 ) by SEQ_4:26; :: thesis: verum

end;

suppose A4: not abs a = 0 ; :: thesis: ( s is convergent & lim s = 0 )

deffunc H₁( Element of NAT ) -> Element of REAL = (abs a) to_power ($1 + 1);
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: now

let n be Element of NAT ; :: thesis: s1 . n = abs (s . n)
thus s1 . n = (abs a) to_power (n + 1) by A5
.= abs (a to_power (n + 1)) by Th2
.= abs (s . n) by A2 ; :: thesis: verum

end;

A7: abs a > 0 by A4, COMPLEX1:46;
then lim s1 = 0 by A1, A5, Th1;
then A8: lim (abs s) = 0 by A6, SEQ_1:12;
s1 is convergent by A1, A7, A5, Th1;
then abs s is convergent by A6, SEQ_1:12;
hence ( s is convergent & lim s = 0 ) by A8, SEQ_4:15; :: thesis: verum

end;

end;

end;

hence ( s is convergent & lim s = 0 ) ; :: thesis: verum