let seq be Complex_Sequence; :: thesis: for z being Element of COMPLEX st |.z.| < 1 & ( for n being Element of NAT holds seq . n = z #N (n + 1) ) holds
( seq is convergent & lim seq = 0c )
let z be Element of COMPLEX ; :: thesis: ( |.z.| < 1 & ( for n being Element of NAT holds seq . n = z #N (n + 1) ) implies ( seq is convergent & lim seq = 0c ) )
assume A1: ( |.z.| < 1 & ( for n being Element of NAT holds seq . n = z #N (n + 1) ) ) ; :: thesis: ( seq is convergent & lim seq = 0c )
then A2: seq . 0 = z #N (0 + 1)
.= z by NEWTON:10 ;

A3: now

let n be Element of NAT ; :: thesis: seq . (n + 1) = (seq . n) * z
thus seq . (n + 1) = z #N ((n + 1) + 1) by A1
.= (z #N (n + 1)) * z by NEWTON:11
.= (seq . n) * z by A1 ; :: thesis: verum

end;

A4: now

assume A5: |.z.| <> 0 ; :: thesis: ( seq is convergent & lim seq = 0c )
0 <= |.z.| by COMPLEX1:132;
hence ( seq is convergent & lim seq = 0c ) by A1, A2, A3, A5, Th43; :: thesis: verum

end;

now

assume |.z.| = 0 ; :: thesis: ( seq is convergent & seq is convergent & lim seq = 0c )
then A6: z = 0c by COMPLEX1:131;

A7: now

let n be Element of NAT ; :: thesis: seq . n = 0c
thus seq . n = 0c #N (n + 1) by A1, A6
.= ((0c GeoSeq ) . n) * 0c by Def1
.= 0c ; :: thesis: verum

end;

hence seq is convergent by COMSEQ_2:9; :: thesis: ( seq is convergent & lim seq = 0c )
thus ( seq is convergent & lim seq = 0c ) by A7, COMSEQ_2:9, COMSEQ_2:10; :: thesis: verum

end;

hence ( seq is convergent & lim seq = 0c ) by A4; :: thesis: verum