for CNS being ComplexNormSpace
for x being Point of CNS
for S being sequence of CNS st S is convergent holds
S - x is convergent