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

A4: now

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

end;

then A5: s is V8() by VALUED_0:def 18;
s . 0 = 0 by A4;
hence ( s is convergent & lim s = 0 ) by A5, SEQ_4:41; :: thesis: verum

end;

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

then A6: abs a > 0 by COMPLEX1:132;
deffunc H₁( Element of NAT ) -> Element of REAL = (abs a) to_power ($1 + 1);
consider s1 being Real_Sequence such that
A7: for n being Element of NAT holds s1 . n = H₁(n) from SEQ_1:sch 1();
A8: ( s1 is convergent & lim s1 = 0 ) by A1, A6, A7, Th1;

now

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

end;

then ( abs s is convergent & lim (abs s) = 0 ) by A8, SEQ_1:16;
hence ( s is convergent & lim s = 0 ) by SEQ_4:28; :: thesis: verum

end;

end;

end;

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