let t be Complex_Sequence; :: thesis: ( t = s *' implies t is convergent )
assume A1: t = s *' ; :: thesis: t is convergent
consider g being Element of COMPLEX such that
A2: for p being Real st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.((s . m) - g).| < p by Def5;
reconsider z = g *' as Element of COMPLEX ;
take r = g *' ; :: according to COMSEQ_2:def 5 :: thesis: for p being Real st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.((t . m) - r).| < p
let p be Real; :: thesis: ( 0 < p implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.((t . m) - r).| < p )
assume 0 < p ; :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.((t . m) - r).| < p
then consider n being Element of NAT such that
A3: for m being Element of NAT st n <= m holds
|.((s . m) - g).| < p by A2;
take n ; :: thesis: for m being Element of NAT st n <= m holds
|.((t . m) - r).| < p
let m be Element of NAT ; :: thesis: ( n <= m implies |.((t . m) - r).| < p )
assume A4: n <= m ; :: thesis: |.((t . m) - r).| < p
|.(((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