let X be ComplexUnitarySpace; :: thesis: for seq1, seq2 being sequence of X st seq1 is convergent & ex k being Nat st
for n being Nat st k <= n holds
seq2 . n = seq1 . n holds
seq2 is convergent
let seq1, seq2 be sequence of X; :: thesis: ( seq1 is convergent & ex k being Nat st
for n being Nat st k <= n holds
seq2 . n = seq1 . n implies seq2 is convergent )
assume that
A1: seq1 is convergent and
A2: ex k being Nat st
for n being Nat st k <= n holds
seq2 . n = seq1 . n ; :: thesis: seq2 is convergent
consider k being Nat such that
A3: for n being Nat st n >= k holds
seq2 . n = seq1 . n by A2;
consider g being Point of X such that
A4: for r being Real st r > 0 holds
ex m being Nat st
for n being Nat st n >= m holds
dist ((seq1 . n),g) < r by A1;
take h = g; :: according to CLVECT_2:def 1 :: thesis: for r being Real st r > 0 holds
ex m being Nat st
for n being Nat st n >= m holds
dist ((seq2 . n),h) < r
let r be Real; :: thesis: ( r > 0 implies ex m being Nat st
for n being Nat st n >= m holds
dist ((seq2 . n),h) < r )
assume r > 0 ; :: thesis: ex m being Nat st
for n being Nat st n >= m holds
dist ((seq2 . n),h) < r
then consider m1 being Nat such that
A5: for n being Nat st n >= m1 holds
dist ((seq1 . n),h) < r by A4;

A6: now :: thesis: ( m1 <= k implies ex m being Nat st
for n being Nat st n >= m holds
dist ((seq2 . n),h) < r )

assume A7: m1 <= k ; :: thesis: ex m being Nat st
for n being Nat st n >= m holds
dist ((seq2 . n),h) < r
take m = k; :: thesis: for n being Nat st n >= m holds
dist ((seq2 . n),h) < r
let n be Nat; :: thesis: ( n >= m implies dist ((seq2 . n),h) < r )
assume A8: n >= m ; :: thesis: dist ((seq2 . n),h) < r
then n >= m1 by A7, XXREAL_0:2;
then dist ((seq1 . n),g) < r by A5;
hence dist ((seq2 . n),h) < r by A3, A8; :: thesis: verum

end;

now :: thesis: ( k <= m1 implies ex m being Nat st
for n being Nat st n >= m holds
dist ((seq2 . n),h) < r )

assume A9: k <= m1 ; :: thesis: ex m being Nat st
for n being Nat st n >= m holds
dist ((seq2 . n),h) < r
take m = m1; :: thesis: for n being Nat st n >= m holds
dist ((seq2 . n),h) < r
let n be Nat; :: thesis: ( n >= m implies dist ((seq2 . n),h) < r )
assume A10: n >= m ; :: thesis: dist ((seq2 . n),h) < r
then seq2 . n = seq1 . n by A3, A9, XXREAL_0:2;
hence dist ((seq2 . n),h) < r by A5, A10; :: thesis: verum

end;

hence ex m being Nat st
for n being Nat st n >= m holds
dist ((seq2 . n),h) < r by A6; :: thesis: verum