let X be ComplexUnitarySpace; :: thesis: for seq1, seq2 being sequence of X holds
( seq1 is_compared_to seq2 iff for r being Real st r > 0 holds
ex m being Element of NAT st
for n being Element of NAT st n >= m holds
||.((seq1 . n) - (seq2 . n)).|| < r )
let seq1, seq2 be sequence of X; :: thesis: ( seq1 is_compared_to seq2 iff for r being Real st r > 0 holds
ex m being Element of NAT st
for n being Element of NAT st n >= m holds
||.((seq1 . n) - (seq2 . n)).|| < r )
thus ( seq1 is_compared_to seq2 implies for r being Real st r > 0 holds
ex m being Element of NAT st
for n being Element of NAT st n >= m holds
||.((seq1 . n) - (seq2 . n)).|| < r ) :: thesis: ( ( for r being Real st r > 0 holds
ex m being Element of NAT st
for n being Element of NAT st n >= m holds
||.((seq1 . n) - (seq2 . n)).|| < r ) implies seq1 is_compared_to seq2 )

proof

assume A1: seq1 is_compared_to seq2 ; :: thesis: for r being Real st r > 0 holds
ex m being Element of NAT st
for n being Element of NAT st n >= m holds
||.((seq1 . n) - (seq2 . n)).|| < r
let r be Real; :: thesis: ( r > 0 implies ex m being Element of NAT st
for n being Element of NAT st n >= m holds
||.((seq1 . n) - (seq2 . n)).|| < r )
assume r > 0 ; :: thesis: ex m being Element of NAT st
for n being Element of NAT st n >= m holds
||.((seq1 . n) - (seq2 . n)).|| < r
then consider m1 being Element of NAT such that
A2: for n being Element of NAT st n >= m1 holds
dist (seq1 . n),(seq2 . n) < r by A1, Def9;
take m = m1; :: thesis: for n being Element of NAT st n >= m holds
||.((seq1 . n) - (seq2 . n)).|| < r
let n be Element of NAT ; :: thesis: ( n >= m implies ||.((seq1 . n) - (seq2 . n)).|| < r )
assume n >= m ; :: thesis: ||.((seq1 . n) - (seq2 . n)).|| < r
then dist (seq1 . n),(seq2 . n) < r by A2;
hence ||.((seq1 . n) - (seq2 . n)).|| < r by CSSPACE:def 16; :: thesis: verum

end;

( ( for r being Real st r > 0 holds
ex m being Element of NAT st
for n being Element of NAT st n >= m holds
||.((seq1 . n) - (seq2 . n)).|| < r ) implies seq1 is_compared_to seq2 )

proof

assume A3: for r being Real st r > 0 holds
ex m being Element of NAT st
for n being Element of NAT st n >= m holds
||.((seq1 . n) - (seq2 . n)).|| < r ; :: 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 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
then consider m1 being Element of NAT such that
A4: for n being Element of NAT st n >= m1 holds
||.((seq1 . n) - (seq2 . n)).|| < r by A3;
take m = m1; :: thesis: for n being Element of NAT st n >= m holds
dist (seq1 . n),(seq2 . n) < r
let n be Element of NAT ; :: thesis: ( n >= m implies dist (seq1 . n),(seq2 . n) < r )
assume n >= m ; :: thesis: dist (seq1 . n),(seq2 . n) < r
then ||.((seq1 . n) - (seq2 . n)).|| < r by A4;
hence dist (seq1 . n),(seq2 . n) < r by CSSPACE:def 16; :: thesis: verum

end;

hence ( ( for r being Real st r > 0 holds
ex m being Element of NAT st
for n being Element of NAT st n >= m holds
||.((seq1 . n) - (seq2 . n)).|| < r ) implies seq1 is_compared_to seq2 ) ; :: thesis: verum