let X be ComplexUnitarySpace; :: thesis: for seq1, seq2 being sequence of X st ex k being Element of NAT st
for n being Element of 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 Element of NAT st
for n being Element of NAT st n >= k holds
seq1 . n = seq2 . n implies seq1 is_compared_to seq2 )
assume A1: ex k being Element of NAT st
for n being Element of NAT st n >= k holds
seq1 . n = seq2 . n ; :: thesis: seq1 is_compared_to seq2
let r be Real; :: according to CLVECT_2:def 9 :: thesis: ( r > 0 implies ex m being Element of NAT st
for n being Element of NAT st n >= m holds
dist (seq1 . n),(seq2 . n) < r )
assume A2: r > 0 ; :: thesis: ex m being Element of NAT st
for n being Element of NAT st n >= m holds
dist (seq1 . n),(seq2 . n) < r
consider m being Element of NAT such that
A3: for n being Element of NAT st n >= m holds
seq1 . n = seq2 . n by A1;
take k = m; :: thesis: for n being Element of NAT st n >= k holds
dist (seq1 . n),(seq2 . n) < r
let n be Element of 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 A3
.= 0 by CSSPACE:53 ;
hence dist (seq1 . n),(seq2 . n) < r by A2; :: thesis: verum