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

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