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

hence lim s = g by A2, Def6; :: thesis: verum

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

s is convergent
by A1, Th9;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;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

hence lim s = g by A2, Def6; :: thesis: verum