let r be Real; :: according to BHSP_3:def 1 :: thesis: ( r > 0 implies ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
dist (((seq + x) . n),((seq + x) . m)) < r )
assume r > 0 ; :: thesis: ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
dist (((seq + x) . n),((seq + x) . m)) < r
then consider m1 being Nat such that
A1: for n, m being Nat st n >= m1 & m >= m1 holds
dist ((seq . n),(seq . m)) < r by Def1;
take k = m1; :: thesis: for n, m being Nat st n >= k & m >= k holds
dist (((seq + x) . n),((seq + x) . m)) < r
let n, m be Nat; :: thesis: ( n >= k & m >= k implies dist (((seq + x) . n),((seq + x) . m)) < r )
dist (((seq . n) + x),((seq . m) + x)) <= (dist ((seq . n),(seq . m))) + (dist (x,x)) by BHSP_1:40;
then A2: dist (((seq . n) + x),((seq . m) + x)) <= (dist ((seq . n),(seq . m))) + 0 by BHSP_1:34;
assume ( n >= k & m >= k ) ; :: thesis: dist (((seq + x) . n),((seq + x) . m)) < r
then dist ((seq . n),(seq . m)) < r by A1;
then dist (((seq . n) + x),((seq . m) + x)) < r by A2, XXREAL_0:2;
then dist (((seq + x) . n),((seq . m) + x)) < r by BHSP_1:def 6;
hence dist (((seq + x) . n),((seq + x) . m)) < r by BHSP_1:def 6; :: thesis: verum