let a be Real; :: thesis: for s being Real_Sequence st |.a.| < 1 & ( for n being Nat holds s . n = a to_power (n + 1) ) holds

( s is convergent & lim s = 0 )

let s be Real_Sequence; :: thesis: ( |.a.| < 1 & ( for n being Nat holds s . n = a to_power (n + 1) ) implies ( s is convergent & lim s = 0 ) )

assume that

A1: |.a.| < 1 and

A2: for n being Nat holds s . n = a to_power (n + 1) ; :: thesis: ( s is convergent & lim s = 0 )

( s is convergent & lim s = 0 )

let s be Real_Sequence; :: thesis: ( |.a.| < 1 & ( for n being Nat holds s . n = a to_power (n + 1) ) implies ( s is convergent & lim s = 0 ) )

assume that

A1: |.a.| < 1 and

A2: for n being Nat holds s . n = a to_power (n + 1) ; :: thesis: ( s is convergent & lim s = 0 )

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

hence
( s is convergent & lim s = 0 )
; :: thesis: verumper cases
( |.a.| = 0 or not |.a.| = 0 )
;

end;

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

then A3:
a = 0
by ABSVALUE:2;

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

end;now :: thesis: for n being Nat holds s . n = In (0,REAL)

then
( s is constant & s . 0 = In (0,REAL) )
;let n be Nat; :: thesis: s . n = In (0,REAL)

( 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: verum

end;( 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: verum

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

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

deffunc H_{1}( Nat) -> object = |.a.| to_power ($1 + 1);

consider s1 being Real_Sequence such that

A5: for n being Nat holds s1 . n = H_{1}(n)
from SEQ_1:sch 1();

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;consider s1 being Real_Sequence such that

A5: for n being Nat holds s1 . n = H

A6: now :: thesis: for n being Nat holds s1 . n = |.(s . n).|

A7:
|.a.| > 0
by A4, COMPLEX1:46;let n be Nat; :: thesis: s1 . n = |.(s . n).|

thus s1 . n = |.a.| to_power (n + 1) by A5

.= |.(a to_power (n + 1)).| by Th2

.= |.(s . n).| by A2 ; :: thesis: verum

end;thus s1 . n = |.a.| to_power (n + 1) by A5

.= |.(a to_power (n + 1)).| by Th2

.= |.(s . n).| by A2 ; :: thesis: verum

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