let s be Complex_Sequence; :: thesis: for g being Complex st ( for n being Nat holds s . n = g ) holds
lim s = g
let g be Complex; :: thesis: ( ( for n being Nat holds s . n = g ) implies lim s = g )
assume A1: for n being Nat holds s . n = g ; :: thesis: lim s = g

A2: 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 A3: 0 < p ; :: thesis: ex k being Nat st
for n being Nat st k <= n holds
|.((s . n) - g).| < p
reconsider zz = 0 as Nat ;
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 A3, COMPLEX1:44; :: thesis: verum

end;

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