let X be RealUnitarySpace; :: thesis: for g being Point of X
for seq1, seq2 being sequence of X st seq1 is convergent & lim seq1 = g & seq1 is_compared_to seq2 holds
( seq2 is convergent & lim seq2 = g )
let g be Point of X; :: thesis: for seq1, seq2 being sequence of X st seq1 is convergent & lim seq1 = g & seq1 is_compared_to seq2 holds
( seq2 is convergent & lim seq2 = g )
let seq1, seq2 be sequence of X; :: thesis: ( seq1 is convergent & lim seq1 = g & seq1 is_compared_to seq2 implies ( seq2 is convergent & lim seq2 = g ) )
assume that
A1: ( seq1 is convergent & lim seq1 = g ) and
A2: seq1 is_compared_to seq2 ; :: thesis: ( seq2 is convergent & lim seq2 = g )

A3: now :: 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),g) < 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),g) < r )
assume r > 0 ; :: thesis: ex m being Nat st
for n being Nat st n >= m holds
dist ((seq2 . n),g) < r
then A4: r / 2 > 0 by XREAL_1:215;
then consider m1 being Nat such that
A5: for n being Nat st n >= m1 holds
dist ((seq1 . n),g) < r / 2 by A1, BHSP_2:def 2;
consider m2 being Nat such that
A6: for n being Nat st n >= m2 holds
dist ((seq1 . n),(seq2 . n)) < r / 2 by A2, A4;
reconsider m = m1 + m2 as Nat ;
take m = m; :: thesis: for n being Nat st n >= m holds
dist ((seq2 . n),g) < r
let n be Nat; :: thesis: ( n >= m implies dist ((seq2 . n),g) < r )
assume A7: n >= m ; :: thesis: dist ((seq2 . n),g) < r
m >= m2 by NAT_1:12;
then n >= m2 by A7, XXREAL_0:2;
then A8: dist ((seq1 . n),(seq2 . n)) < r / 2 by A6;
A9: dist ((seq2 . n),g) <= (dist ((seq2 . n),(seq1 . n))) + (dist ((seq1 . n),g)) by BHSP_1:35;
m1 + m2 >= m1 by NAT_1:12;
then n >= m1 by A7, XXREAL_0:2;
then dist ((seq1 . n),g) < r / 2 by A5;
then (dist ((seq2 . n),(seq1 . n))) + (dist ((seq1 . n),g)) < (r / 2) + (r / 2) by A8, XREAL_1:8;
hence dist ((seq2 . n),g) < r by A9, XXREAL_0:2; :: thesis: verum

end;

then seq2 is convergent by BHSP_2:def 1;
hence ( seq2 is convergent & lim seq2 = g ) by A3, BHSP_2:def 2; :: thesis: verum