let X be RealUnitarySpace; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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;

hence lim seq = lim seq9 by A4, Def2; :: thesis: verum

for n being Nat st n >= k holds

seq9 . n = seq . n holds

lim seq = lim seq9

let seq, seq9 be sequence of X; :: thesis: ( 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 ; :: thesis: 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 :: thesis: 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)) < r

seq9 is convergent
by A1, A2, Th2;ex m being Nat st

for n being Nat st n >= m holds

dist ((seq9 . n),(lim seq)) < r

let r be Real; :: thesis: ( 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 ; :: thesis: ex m being Nat st

for n being Nat st n >= m holds

dist ((seq9 . n),(lim seq)) < r

then consider m1 being Nat such that

A5: for n being Nat st n >= m1 holds

dist ((seq . n),(lim seq)) < r by A1, Def2;

for n being Nat st n >= m holds

dist ((seq9 . n),(lim seq)) < r by A6; :: thesis: verum

end;for n being Nat st n >= m holds

dist ((seq9 . n),(lim seq)) < r )

assume r > 0 ; :: thesis: ex m being Nat st

for n being Nat st n >= m holds

dist ((seq9 . n),(lim seq)) < r

then 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 :: thesis: ( m1 <= k implies ex m being Nat st

for n being Nat st n >= m holds

dist ((seq9 . n),(lim seq)) < r )

for n being Nat st n >= m holds

dist ((seq9 . n),(lim seq)) < r )

assume A7:
m1 <= k
; :: thesis: ex m being Nat st

for n being Nat st n >= m holds

dist ((seq9 . n),(lim seq)) < r

take m = k; :: thesis: for n being Nat st n >= m holds

dist ((seq9 . n),(lim seq)) < r

let n be Nat; :: thesis: ( n >= m implies dist ((seq9 . n),(lim seq)) < r )

assume A8: n >= m ; :: thesis: dist ((seq9 . n),(lim seq)) < r

then n >= m1 by A7, XXREAL_0:2;

then dist ((seq . n),(lim seq)) < r by A5;

hence dist ((seq9 . n),(lim seq)) < r by A3, A8; :: thesis: verum

end;for n being Nat st n >= m holds

dist ((seq9 . n),(lim seq)) < r

take m = k; :: thesis: for n being Nat st n >= m holds

dist ((seq9 . n),(lim seq)) < r

let n be Nat; :: thesis: ( n >= m implies dist ((seq9 . n),(lim seq)) < r )

assume A8: n >= m ; :: thesis: dist ((seq9 . n),(lim seq)) < r

then n >= m1 by A7, XXREAL_0:2;

then dist ((seq . n),(lim seq)) < r by A5;

hence dist ((seq9 . n),(lim seq)) < r by A3, A8; :: thesis: verum

now :: thesis: ( k <= m1 implies ex m being Nat st

for n being Nat st n >= m holds

dist ((seq9 . n),(lim seq)) < r )

hence
ex m being Nat st for n being Nat st n >= m holds

dist ((seq9 . n),(lim seq)) < r )

assume A9:
k <= m1
; :: thesis: ex m being Nat st

for n being Nat st n >= m holds

dist ((seq9 . n),(lim seq)) < r

take m = m1; :: thesis: for n being Nat st n >= m holds

dist ((seq9 . n),(lim seq)) < r

let n be Nat; :: thesis: ( n >= m implies dist ((seq9 . n),(lim seq)) < r )

assume A10: n >= m ; :: thesis: dist ((seq9 . n),(lim seq)) < r

then seq9 . n = seq . n by A3, A9, XXREAL_0:2;

hence dist ((seq9 . n),(lim seq)) < r by A5, A10; :: thesis: verum

end;for n being Nat st n >= m holds

dist ((seq9 . n),(lim seq)) < r

take m = m1; :: thesis: for n being Nat st n >= m holds

dist ((seq9 . n),(lim seq)) < r

let n be Nat; :: thesis: ( n >= m implies dist ((seq9 . n),(lim seq)) < r )

assume A10: n >= m ; :: thesis: dist ((seq9 . n),(lim seq)) < r

then seq9 . n = seq . n by A3, A9, XXREAL_0:2;

hence dist ((seq9 . n),(lim seq)) < r by A5, A10; :: thesis: verum

for n being Nat st n >= m holds

dist ((seq9 . n),(lim seq)) < r by A6; :: thesis: verum

hence lim seq = lim seq9 by A4, Def2; :: thesis: verum