for r being Real
for seq, seq1 being Real_Sequence st seq is convergent & ( for n being Nat holds seq1 . n = r - (seq . n) ) holds
( seq1 is convergent & lim seq1 = r - (lim seq) )