let s be Complex_Sequence; :: thesis: ( ex g being Complex st
for n being Nat holds s . n = g implies s is convergent )
reconsider zz = 0 as Nat ;
given g being Complex such that A1: for n being Nat holds s . n = g ; :: thesis: s is convergent
take g ; :: 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
|.((s . m) - g).| < p

now :: thesis: for p being Real st 0 < p holds
ex k being Nat st
for n being Nat st k <= n holds
|.((s . n) - g).| < p

let p be Real; :: thesis: ( 0 < p implies ex k being Nat st
for n being Nat st k <= n holds
|.((s . n) - g).| < p )
assume A2: 0 < p ; :: thesis: ex k being Nat st
for n being Nat st k <= n holds
|.((s . n) - g).| < p
take k = zz; :: thesis: for n being Nat st k <= n holds
|.((s . n) - g).| < p
let n be 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 Nat st
for m being Nat st n <= m holds
|.((s . m) - g).| < p ; :: thesis: verum