for seq, seq9 being Real_Sequence st seq is convergent & seq9 is convergent holds
seq - seq9 is convergent