for S being Real_Sequence
for x being Real st S is convergent holds
( S - x is convergent & lim (S - x) = (lim S) - x )