let s be Complex_Sequence; :: thesis: ( ex g being Element of COMPLEX st
for n being Element of NAT holds s . n = g implies s is convergent )
given g being Element of COMPLEX such that A1: for n being Element of NAT holds s . n = g ; :: thesis: s is convergent
take g ; :: according to COMSEQ_2:def 4 :: 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
|.((s . m) - g).| < p

now

let p be Real; :: thesis: ( 0 < p implies ex k being Element of NAT st
for n being Element of NAT st k <= n holds
|.((s . n) - g).| < p )
assume A2: 0 < p ; :: thesis: ex k being Element of NAT st
for n being Element of NAT st k <= n holds
|.((s . n) - g).| < p
take k = 0 ; :: thesis: for n being Element of NAT st k <= n holds
|.((s . n) - g).| < p
let n be Element of NAT ; :: thesis: ( k <= n implies |.((s . n) - g).| < p )
assume k <= n ; :: thesis: |.((s . n) - g).| < p
s . n = g by A1;
hence |.((s . n) - g).| < p by A2, COMPLEX1:44; :: thesis: verum

end;

hence 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 ; :: thesis: verum