let s be Complex_Sequence; :: thesis: for g being Element of COMPLEX st ( for n being Element of NAT holds s . n = g ) holds
lim s = g
let g be Element of COMPLEX ; :: thesis: ( ( for n being Element of NAT holds s . n = g ) implies lim s = g )
assume A1: for n being Element of NAT holds s . n = g ; :: thesis: lim s = g

A2: 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 A3: 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 A3, COMPLEX1:130; :: thesis: verum

end;

s is convergent by A1, Th9;
hence lim s = g by A2, Def5; :: thesis: verum