let X be RealUnitarySpace; :: thesis: for seq1, seq2 being sequence of X st seq1 is Cauchy & seq1 is_compared_to seq2 holds
seq2 is Cauchy
let seq1, seq2 be sequence of X; :: thesis: ( seq1 is Cauchy & seq1 is_compared_to seq2 implies seq2 is Cauchy )
assume that
A1: seq1 is Cauchy and
A2: seq1 is_compared_to seq2 ; :: thesis: seq2 is Cauchy
let r be Real; :: according to BHSP_3:def 1 :: thesis: ( r > 0 implies ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
dist (seq2 . n),(seq2 . m) < r )
assume r > 0 ; :: thesis: ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
dist (seq2 . n),(seq2 . m) < r
then A3: r / 3 > 0 by XREAL_1:224;
then consider m1 being Element of NAT such that
A4: for n, m being Element of NAT st n >= m1 & m >= m1 holds
dist (seq1 . n),(seq1 . m) < r / 3 by A1, Def1;
consider m2 being Element of NAT such that
A5: for n being Element of NAT st n >= m2 holds
dist (seq1 . n),(seq2 . n) < r / 3 by A2, A3, Def2;
take k = m1 + m2; :: thesis: for n, m being Element of NAT st n >= k & m >= k holds
dist (seq2 . n),(seq2 . m) < r
let n, m be Element of NAT ; :: thesis: ( n >= k & m >= k implies dist (seq2 . n),(seq2 . m) < r )
assume that
A6: n >= k and
A7: m >= k ; :: thesis: dist (seq2 . n),(seq2 . m) < r
m1 + m2 >= m1 by NAT_1:12;
then ( n >= m1 & m >= m1 ) by A6, A7, XXREAL_0:2;
then A8: dist (seq1 . n),(seq1 . m) < r / 3 by A4;
A9: dist (seq2 . n),(seq1 . m) <= (dist (seq2 . n),(seq1 . n)) + (dist (seq1 . n),(seq1 . m)) by BHSP_1:42;
A10: k >= m2 by NAT_1:12;
then n >= m2 by A6, XXREAL_0:2;
then dist (seq1 . n),(seq2 . n) < r / 3 by A5;
then (dist (seq2 . n),(seq1 . n)) + (dist (seq1 . n),(seq1 . m)) < (r / 3) + (r / 3) by A8, XREAL_1:10;
then A11: dist (seq2 . n),(seq1 . m) < (r / 3) + (r / 3) by A9, XXREAL_0:2;
A12: dist (seq2 . n),(seq2 . m) <= (dist (seq2 . n),(seq1 . m)) + (dist (seq1 . m),(seq2 . m)) by BHSP_1:42;
m >= m2 by A7, A10, XXREAL_0:2;
then dist (seq1 . m),(seq2 . m) < r / 3 by A5;
then (dist (seq2 . n),(seq1 . m)) + (dist (seq1 . m),(seq2 . m)) < ((r / 3) + (r / 3)) + (r / 3) by A11, XREAL_1:10;
hence dist (seq2 . n),(seq2 . m) < r by A12, XXREAL_0:2; :: thesis: verum