let X be Complex_Banach_Algebra; :: thesis: for s being sequence of X
for z being Element of X st ( for n being Element of 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 Element of NAT holds s . n = z ) holds
lim s = z
let z be Element of X; :: thesis: ( ( for n being Element of NAT holds s . n = z ) implies lim s = z )
assume A1: for n being Element of NAT holds s . n = z ; :: thesis: lim s = z

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) - z).|| < 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) - z).|| < p
take k = 0 ; :: thesis: for n being Element of NAT st k <= n holds
||.((s . n) - z).|| < p
let n be Element of 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;

then s is convergent by CLVECT_1:def 15;
hence lim s = z by A2, CLVECT_1:def 16; :: thesis: verum