for X being ComplexUnitarySpace
for x being Point of X
for seq being sequence of X st seq is Cauchy holds
seq + x is Cauchy