let X be RealUnitarySpace; :: thesis: for seq, seq1 being sequence of X st seq is Cauchy & ex k being Nat st seq = seq1 ^\ k holds
seq1 is Cauchy
let seq, seq1 be sequence of X; :: thesis: ( seq is Cauchy & ex k being Nat st seq = seq1 ^\ k implies seq1 is Cauchy )
assume that
A1: seq is Cauchy and
A2: ex k being Nat st seq = seq1 ^\ k ; :: thesis: seq1 is Cauchy
consider k being Nat such that
A3: seq = seq1 ^\ k by A2;
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 . n),(seq1 . m)) < r )
assume r > 0 ; :: thesis: ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
dist ((seq1 . n),(seq1 . m)) < r
then consider l1 being Nat such that
A4: for n, m being Nat st n >= l1 & m >= l1 holds
dist ((seq . n),(seq . m)) < r by A1;
take l = l1 + k; :: thesis: for n, m being Nat st n >= l & m >= l holds
dist ((seq1 . n),(seq1 . m)) < r
let n, m be Nat; :: thesis: ( n >= l & m >= l implies dist ((seq1 . n),(seq1 . m)) < r )
assume that
A5: n >= l and
A6: m >= l ; :: thesis: dist ((seq1 . n),(seq1 . m)) < r
consider m1 being Nat such that
A7: n = (l1 + k) + m1 by A5, NAT_1:10;
reconsider m1 = m1 as Nat ;
n - k = l1 + m1 by A7;
then consider l2 being Nat such that
A8: l2 = n - k ;
consider m2 being Nat such that
A9: m = (l1 + k) + m2 by A6, NAT_1:10;
reconsider m2 = m2 as Nat ;
m - k = l1 + m2 by A9;
then consider l3 being Nat such that
A10: l3 = m - k ;

A11: now :: thesis: not l2 < l1

assume l2 < l1 ; :: thesis: contradiction
then l2 + k < l1 + k by XREAL_1:6;
hence contradiction by A5, A8; :: thesis: verum

end;

A12: l2 + k = n by A8;

now :: thesis: not l3 < l1

assume l3 < l1 ; :: thesis: contradiction
then l3 + k < l1 + k by XREAL_1:6;
hence contradiction by A6, A10; :: thesis: verum

end;

then dist ((seq . l2),(seq . l3)) < r by A4, A11;
then A13: dist ((seq1 . n),(seq . l3)) < r by A3, A12, NAT_1:def 3;
l3 + k = m by A10;
hence dist ((seq1 . n),(seq1 . m)) < r by A3, A13, NAT_1:def 3; :: thesis: verum