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 A3, CLVECT_1:107; :: thesis: verum
end;
then s is convergent ;
hence lim s = z by A2, CLVECT_1:def 16; :: thesis: verum