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

A11: now

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

end;

consider l3 being Element of NAT such that
A12: l3 = m - k by A9;

A13: now

assume l3 < l1 ; :: thesis: contradiction
then l3 + k < l1 + k by XREAL_1:8;
hence contradiction by A5, A12; :: thesis: verum

end;

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