let t be Complex_Sequence; :: thesis: ( t = s *' implies t is convergent )
assume A1: t = s *' ; :: thesis: t is convergent
consider g being Complex such that
A2: for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((s . m) - g).| < p by Def5;
reconsider z = g *' as Element of COMPLEX by XCMPLX_0:def 2;
take r = z; :: according to COMSEQ_2:def 5 :: thesis: for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((t . m) - r).| < p
let p be Real; :: thesis: ( 0 < p implies ex n being Nat st
for m being Nat st n <= m holds
|.((t . m) - r).| < p )
assume 0 < p ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
|.((t . m) - r).| < p
then consider n being Nat such that
A3: for m being Nat st n <= m holds
|.((s . m) - g).| < p by A2;
take n ; :: thesis: for m being Nat st n <= m holds
|.((t . m) - r).| < p
let m be Nat; :: thesis: ( n <= m implies |.((t . m) - r).| < p )
assume A4: n <= m ; :: thesis: |.((t . m) - r).| < p
m in NAT by ORDINAL1:def 12;
then |.(((s *') . m) - r).| = |.(((s . m) *') - (g *')).| by Def2
.= |.(((s . m) - g) *').| by COMPLEX1:34
.= |.((s . m) - g).| by COMPLEX1:53 ;
hence |.((t . m) - r).| < p by A3, A4, A1; :: thesis: verum