let X be ComplexUnitarySpace; :: thesis: for x being Point of X
for seq being sequence of X st seq is Cauchy holds
seq - x is Cauchy
let x be Point of X; :: thesis: for seq being sequence of X st seq is Cauchy holds
seq - x is Cauchy
let seq be sequence of X; :: thesis: ( seq is Cauchy implies seq - x is Cauchy )
assume seq is Cauchy ; :: thesis: seq - x is Cauchy
then seq + (- x) is Cauchy by Th63;
hence seq - x is Cauchy by CSSPACE:71; :: thesis: verum