for RNS being RealNormSpace
for x being Point of RNS
for S being sequence of RNS st S is convergent holds
S - x is convergent