let X be RealUnitarySpace; :: 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 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 (seq . n),(seq . n) < r )
assume A1: r > 0 ; :: thesis: ex m being Element of NAT st
for n being Element of NAT st n >= m holds
dist (seq . n),(seq . n) < r
take m = 0 ; :: thesis: for n being Element of NAT st n >= m holds
dist (seq . n),(seq . n) < r
let n be Element of 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, BHSP_1:41; :: thesis: verum