for CNS being ComplexNormSpace
for x being Point of CNS
for S being sequence of CNS st S is convergent holds
lim (S - x) = (lim S) - x