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