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
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
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 ; :: thesis: verum
end;
then s is convergent ;
hence lim s = z by ; :: thesis: verum