let X be RealUnitarySpace; :: thesis: for seq1, seq2 being sequence of X st ex k being Nat st
for n being Nat st n >= k holds
seq1 . n = seq2 . n holds
seq1 is_compared_to seq2
let seq1, seq2 be sequence of X; :: thesis: ( ex k being Nat st
for n being Nat st n >= k holds
seq1 . n = seq2 . n implies seq1 is_compared_to seq2 )
assume ex k being Nat st
for n being Nat st n >= k holds
seq1 . n = seq2 . n ; :: thesis: seq1 is_compared_to seq2
then consider m being Nat such that
A1: for n being Nat st n >= m holds
seq1 . n = seq2 . n ;
let r be Real; :: according to BHSP_3:def 2 :: thesis: ( r > 0 implies ex m being Nat st
for n being Nat st n >= m holds
dist ((seq1 . n),(seq2 . n)) < r )
assume A2: r > 0 ; :: thesis: ex m being Nat st
for n being Nat st n >= m holds
dist ((seq1 . n),(seq2 . n)) < r
take k = m; :: thesis: for n being Nat st n >= k holds
dist ((seq1 . n),(seq2 . n)) < r
let n be Nat; :: thesis: ( n >= k implies dist ((seq1 . n),(seq2 . n)) < r )
assume n >= k ; :: thesis: dist ((seq1 . n),(seq2 . n)) < r
then dist ((seq1 . n),(seq2 . n)) = dist ((seq1 . n),(seq1 . n)) by A1
.= 0 by BHSP_1:34 ;
hence dist ((seq1 . n),(seq2 . n)) < r by A2; :: thesis: verum