for X being ComplexUnitarySpace
for seq, seq1 being sequence of X st seq is Cauchy & ex k being Nat st seq = seq1 ^\ k holds
seq1 is Cauchy