let X be Complex_Banach_Algebra; :: thesis: for s being sequence of X

for z being Element of X st ( for n being Nat holds s . n = z ) holds

lim s = z

let s be sequence of X; :: thesis: for z being Element of X st ( for n being Nat holds s . n = z ) holds

lim s = z

let z be Element of X; :: thesis: ( ( for n being Nat holds s . n = z ) implies lim s = z )

assume A1: for n being Nat holds s . n = z ; :: thesis: lim s = z

hence lim s = z by A2, CLVECT_1:def 16; :: thesis: verum

for z being Element of X st ( for n being Nat holds s . n = z ) holds

lim s = z

let s be sequence of X; :: thesis: for z being Element of X st ( for n being Nat holds s . n = z ) holds

lim s = z

let z be Element of X; :: thesis: ( ( for n being Nat holds s . n = z ) implies lim s = z )

assume A1: for n being Nat holds s . n = z ; :: thesis: lim s = z

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) - z).|| < p

then
s is convergent
;ex k being Nat st

for n being Nat st k <= n holds

||.((s . n) - z).|| < p

let p be Real; :: thesis: ( 0 < p implies ex k being Nat st

for n being Nat st k <= n holds

||.((s . n) - z).|| < p )

assume A3: 0 < p ; :: thesis: ex k being Nat st

for n being Nat st k <= n holds

||.((s . n) - z).|| < p

reconsider k = 0 as Nat ;

take k = k; :: thesis: for n being Nat st k <= n holds

||.((s . n) - z).|| < p

let n be Nat; :: thesis: ( k <= n implies ||.((s . n) - z).|| < p )

assume k <= n ; :: thesis: ||.((s . n) - z).|| < p

s . n = z by A1;

hence ||.((s . n) - z).|| < p by A3, CLVECT_1:107; :: thesis: verum

end;for n being Nat st k <= n holds

||.((s . n) - z).|| < p )

assume A3: 0 < p ; :: thesis: ex k being Nat st

for n being Nat st k <= n holds

||.((s . n) - z).|| < p

reconsider k = 0 as Nat ;

take k = k; :: thesis: for n being Nat st k <= n holds

||.((s . n) - z).|| < p

let n be Nat; :: thesis: ( k <= n implies ||.((s . n) - z).|| < p )

assume k <= n ; :: thesis: ||.((s . n) - z).|| < p

s . n = z by A1;

hence ||.((s . n) - z).|| < p by A3, CLVECT_1:107; :: thesis: verum

hence lim s = z by A2, CLVECT_1:def 16; :: thesis: verum