let X be RealUnitarySpace; for seq, seq9 being sequence of X st seq is convergent & ex k being Nat st
for n being Nat st n >= k holds
seq9 . n = seq . n holds
lim seq = lim seq9
let seq, seq9 be sequence of X; ( seq is convergent & ex k being Nat st
for n being Nat st n >= k holds
seq9 . n = seq . n implies lim seq = lim seq9 )
assume that
A1:
seq is convergent
and
A2:
ex k being Nat st
for n being Nat st n >= k holds
seq9 . n = seq . n
; lim seq = lim seq9
consider k being Nat such that
A3:
for n being Nat st n >= k holds
seq9 . n = seq . n
by A2;
A4:
now for r being Real st r > 0 holds
ex m being Nat st
for n being Nat st n >= m holds
dist ((seq9 . n),(lim seq)) < rlet r be
Real;
( r > 0 implies ex m being Nat st
for n being Nat st n >= m holds
dist ((seq9 . n),(lim seq)) < r )assume
r > 0
;
ex m being Nat st
for n being Nat st n >= m holds
dist ((seq9 . n),(lim seq)) < rthen consider m1 being
Nat such that A5:
for
n being
Nat st
n >= m1 holds
dist (
(seq . n),
(lim seq))
< r
by A1, Def2;
A6:
now ( m1 <= k implies ex m being Nat st
for n being Nat st n >= m holds
dist ((seq9 . n),(lim seq)) < r )end; hence
ex
m being
Nat st
for
n being
Nat st
n >= m holds
dist (
(seq9 . n),
(lim seq))
< r
by A6;
verum end;
seq9 is convergent
by A1, A2, Th2;
hence
lim seq = lim seq9
by A4, Def2; verum