for seq1, seq2 being ExtREAL_sequence
for r being R_eal st r in REAL & ( for n being Nat holds seq1 . n = r + (seq2 . n) ) holds
( lim_inf seq1 = r + (lim_inf seq2) & lim_sup seq1 = r + (lim_sup seq2) )