let X be ComplexUnitarySpace; :: thesis: for seq being sequence of X holds seq is_compared_to seq
let seq be sequence of X; :: thesis: seq is_compared_to seq
let r be Real; :: according to CLVECT_2:def 9 :: thesis: ( r > 0 implies ex m being Nat st
for n being Nat st n >= m holds
dist ((seq . n),(seq . n)) < r )
assume A1: r > 0 ; :: thesis: ex m being Nat st
for n being Nat st n >= m holds
dist ((seq . n),(seq . n)) < r
take m = 0 ; :: thesis: for n being Nat st n >= m holds
dist ((seq . n),(seq . n)) < r
let n be Nat; :: thesis: ( n >= m implies dist ((seq . n),(seq . n)) < r )
assume n >= m ; :: thesis: dist ((seq . n),(seq . n)) < r
thus dist ((seq . n),(seq . n)) < r by A1, CSSPACE:50; :: thesis: verum