let X be RealUnitarySpace; :: thesis: for seq, seq' being sequence of X st seq is convergent & ex k being Element of NAT st
for n being Element of NAT st n >= k holds
seq' . n = seq . n holds
lim seq = lim seq'
let seq, seq' be sequence of X; :: thesis: ( seq is convergent & ex k being Element of NAT st
for n being Element of NAT st n >= k holds
seq' . n = seq . n implies lim seq = lim seq' )
assume that
A1: seq is convergent and
A2: ex k being Element of NAT st
for n being Element of NAT st n >= k holds
seq' . n = seq . n ; :: thesis: lim seq = lim seq'
A3: seq' is convergent by A1, A2, Th2;
consider k being Element of NAT such that
A4: for n being Element of NAT st n >= k holds
seq' . n = seq . n by A2;

now

let r be Real; :: thesis: ( r > 0 implies ex m being Element of NAT st
for n being Element of NAT st n >= m holds
dist (seq' . n),(lim seq) < r )
assume r > 0 ; :: thesis: ex m being Element of NAT st
for n being Element of NAT st n >= m holds
dist (seq' . n),(lim seq) < r
then consider m1 being Element of NAT such that
A5: for n being Element of NAT st n >= m1 holds
dist (seq . n),(lim seq) < r by A1, Def2;

A6: now

assume A7: k <= m1 ; :: thesis: ex m being Element of NAT st
for n being Element of NAT st n >= m holds
dist (seq' . n),(lim seq) < r
take m = m1; :: thesis: for n being Element of NAT st n >= m holds
dist (seq' . n),(lim seq) < r
let n be Element of NAT ; :: thesis: ( n >= m implies dist (seq' . n),(lim seq) < r )
assume A8: n >= m ; :: thesis: dist (seq' . n),(lim seq) < r
then seq' . n = seq . n by A4, A7, XXREAL_0:2;
hence dist (seq' . n),(lim seq) < r by A5, A8; :: thesis: verum

end;

now

assume A9: m1 <= k ; :: thesis: ex m being Element of NAT st
for n being Element of NAT st n >= m holds
dist (seq' . n),(lim seq) < r
take m = k; :: thesis: for n being Element of NAT st n >= m holds
dist (seq' . n),(lim seq) < r
let n be Element of NAT ; :: thesis: ( n >= m implies dist (seq' . n),(lim seq) < r )
assume A10: n >= m ; :: thesis: dist (seq' . n),(lim seq) < r
then n >= m1 by A9, XXREAL_0:2;
then dist (seq . n),(lim seq) < r by A5;
hence dist (seq' . n),(lim seq) < r by A4, A10; :: thesis: verum

end;

hence ex m being Element of NAT st
for n being Element of NAT st n >= m holds
dist (seq' . n),(lim seq) < r by A6; :: thesis: verum

end;

hence lim seq = lim seq' by A3, Def2; :: thesis: verum