let a be Real; :: thesis:
let s be Real_Sequence; :: thesis:
assume that
A1: |.a.| < 1 and
A2: for n being Nat holds s . n = a to_power (n + 1) ; :: thesis:

now :: thesis:

per cases = 0 or not |.a.| = 0 ) ;

suppose |.a.| = 0 ; :: thesis:

then A3: a = 0 by ABSVALUE:2;

now :: thesis:

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

end;

then ( s is constant & s . 0 = In (0,REAL) ) ;
hence ( s is convergent & lim s = 0 ) by SEQ_4:26; :: thesis:

end;

suppose A4: not |.a.| = 0 ; :: thesis:

deffunc H₁( Nat) -> object = |.a.| to_power ($1 + 1);
consider s1 being Real_Sequence such that
A5: for n being Nat holds s1 . n = H₁(n) from SEQ_1:sch 1();

A6: now :: thesis:

let n be Nat; :: thesis:
thus s1 . n = |.a.| to_power (n + 1) by A5
.= |.(a to_power (n + 1)).| by Th2
.= |.(s . n).| by A2 ; :: thesis:

end;

A7: |.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:

end;

end;

end;

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