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 (((seq1 - seq2) . n),((seq1 - seq2) . m)) < r )
assume r > 0 ; :: thesis: ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
dist (((seq1 - seq2) . n),((seq1 - seq2) . m)) < r
then A1: r / 2 > 0 by XREAL_1:215;
then consider m1 being Nat such that
A2: for n, m being Nat st n >= m1 & m >= m1 holds
dist ((seq1 . n),(seq1 . m)) < r / 2 by Def1;
consider m2 being Nat such that
A3: for n, m being Nat st n >= m2 & m >= m2 holds
dist ((seq2 . n),(seq2 . m)) < r / 2 by A1, Def1;
take k = m1 + m2; :: thesis: for n, m being Nat st n >= k & m >= k holds
dist (((seq1 - seq2) . n),((seq1 - seq2) . m)) < r
let n, m be Nat; :: thesis: ( n >= k & m >= k implies dist (((seq1 - seq2) . n),((seq1 - seq2) . m)) < r )
assume A4: ( n >= k & m >= k ) ; :: thesis: dist (((seq1 - seq2) . n),((seq1 - seq2) . m)) < r
k >= m2 by NAT_1:12;
then ( n >= m2 & m >= m2 ) by A4, XXREAL_0:2;
then A5: dist ((seq2 . n),(seq2 . m)) < r / 2 by A3;
dist (((seq1 - seq2) . n),((seq1 - seq2) . m)) = dist (((seq1 . n) - (seq2 . n)),((seq1 - seq2) . m)) by NORMSP_1:def 3
.= dist (((seq1 . n) - (seq2 . n)),((seq1 . m) - (seq2 . m))) by NORMSP_1:def 3 ;
then A6: dist (((seq1 - seq2) . n),((seq1 - seq2) . m)) <= (dist ((seq1 . n),(seq1 . m))) + (dist ((seq2 . n),(seq2 . m))) by BHSP_1:41;
m1 + m2 >= m1 by NAT_1:12;
then ( n >= m1 & m >= m1 ) by A4, XXREAL_0:2;
then dist ((seq1 . n),(seq1 . m)) < r / 2 by A2;
then (dist ((seq1 . n),(seq1 . m))) + (dist ((seq2 . n),(seq2 . m))) < (r / 2) + (r / 2) by A5, XREAL_1:8;
hence dist (((seq1 - seq2) . n),((seq1 - seq2) . m)) < r by A6, XXREAL_0:2; :: thesis: verum